minpoly.eq_X_sub_C
theorem minpoly.eq_X_sub_C :
∀ {A : Type u_1} (B : Type u_2) [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] [inst_3 : Nontrivial B]
(a : A), minpoly A ((algebraMap A B) a) = Polynomial.X - Polynomial.C a
This theorem states that if `B/K` is a nontrivial algebra over a field, and `x` is an element of `K`, then the minimal polynomial of the algebraic embedding of `x` into `B` (denoted by `algebraMap K B x`) is `X - C x`. Here, `X` represents the polynomial variable (also known as the indeterminate) and `C x` is the constant polynomial `x`. This result is a fundamental fact about minimal polynomials in field theory and algebra.
More concisely: The minimal polynomial of the algebraic embedding of an element `x` in a field extension `B/K` is `X - C x`, where `C x` is the constant polynomial equal to `x`.
|
minpoly.coeff_zero_ne_zero
theorem minpoly.coeff_zero_ne_zero :
∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : IsDomain B] [inst_3 : Algebra A B]
{x : B}, IsIntegral A x → x ≠ 0 → (minpoly A x).coeff 0 ≠ 0
The theorem `minpoly.coeff_zero_ne_zero` states that the minimal polynomial of a nonzero element has a nonzero constant coefficient. More specifically, for any field `A`, any ring `B` that is also a domain, and any element `x` of `B` that is integral over `A`, if `x` is not equal to zero, then the coefficient of `x^0` (the constant term) in the minimal polynomial of `x` over `A` is not equal to zero.
More concisely: If `x` is a nonzero element integral over a field `A` in a domain `B`, then the constant term of `x`'s minimal polynomial over `A` is nonzero.
|
minpoly.root
theorem minpoly.root :
∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : IsDomain B] [inst_3 : Algebra A B]
{x : B}, IsIntegral A x → ∀ {y : A}, (minpoly A x).IsRoot y → (algebraMap A B) y = x
This theorem states that if `L/K` represents a field extension, and an element `y` in `K` is a root of the minimal polynomial of an element `x` in `L`, then the algebraic map from `A` to `B` applied to `y` equals `x`. In simpler terms, under the conditions of a field extension and `y` being a root of the minimal polynomial of `x`, the mapping function transforms `y` to `x`.
More concisely: If `L/K` is a field extension and `x` in `L` has `y` in `K` as a root of its minimal polynomial, then the image of `y` under the algebraic map from `L` to `K(x)` equals `x`.
|
minpoly.degree_le_of_ne_zero
theorem minpoly.degree_le_of_ne_zero :
∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B)
{p : Polynomial A}, p ≠ 0 → (Polynomial.aeval x) p = 0 → (minpoly A x).degree ≤ p.degree
This theorem states that if `x` is a root of a nonzero polynomial `p` in an `A`-field `B` with ring structure and `A`-algebra structure, then the degree of `p` is at least the degree of the minimal polynomial of `x`. In other words, if `p` is not zero and `p` evaluated at `x` equals zero (meaning `x` is a root of `p`), then the degree of the minimal polynomial of `x` (in the field `A`) is less than or equal to the degree of `p`. A related theorem, `minpoly.IsIntegrallyClosed.degree_le_of_ne_zero`, contains less restrictive conditions on `A` but more restrictive conditions on `B`.
More concisely: If `x` is a root of a nonzero polynomial `p` in an `A`-field `B` with ring and `A`-algebra structures, then the degree of `p` is at least the degree of the minimal polynomial of `x` over `A`.
|
minpoly.unique
theorem minpoly.unique :
∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B)
{p : Polynomial A},
p.Monic →
(Polynomial.aeval x) p = 0 →
(∀ (q : Polynomial A), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree) → p = minpoly A x
The theorem `minpoly.unique` states that the minimal polynomial of an element `x` is uniquely determined by its defining property. That is, if there exists another monic polynomial of minimal degree for which `x` is a root, then that polynomial must be equal to the minimal polynomial of `x`. This theorem applies in the context where `A` is a field, `B` is a ring, and there exists an algebra structure from `A` to `B`. Note that there exists a related theorem, `minpoly.IsIntegrallyClosed.Minpoly.unique`, which provides a similar uniqueness property under a different set of assumptions on `A` and `B`.
More concisely: Given a field `A`, a ring `B`, and an algebra structure from `A` to `B`, the minimal polynomial of an element `x` in `B` is uniquely determined as the monic polynomial of minimal degree with `x` as a root.
|
minpoly_algEquiv_toLinearMap
theorem minpoly_algEquiv_toLinearMap :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CommRing L] [inst_2 : IsDomain L] [inst_3 : Algebra K L]
(σ : L ≃ₐ[K] L), IsOfFinOrder σ → minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1
The theorem `minpoly_algEquiv_toLinearMap` states that for any field `K`, commutative ring `L`, and given that `L` is a domain and an algebra over `K`, if `σ` is an algebraic equivalence from `L` to `L` and is of finite order, then the minimal polynomial over `K` of `σ` is `X` raised to the power of the order of `σ` minus one, where `X` is the polynomial variable and "order of `σ`" refers to the smallest positive integer `n` such that `σ^n = 1` (or `0` if no such `n` exists).
More concisely: If `σ: L → L` is a finite order algebraic equivalence over a field `K` from a commutative domain ring `L` to itself as an algebra over `K`, then the minimal polynomial of `σ` over `K` is `X^(order(σ)-1)`.
|
minpoly.dvd_map_of_isScalarTower
theorem minpoly.dvd_map_of_isScalarTower :
∀ (A : Type u_3) (K : Type u_4) {R : Type u_5} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing R]
[inst_3 : Algebra A K] [inst_4 : Algebra A R] [inst_5 : Algebra K R] [inst_6 : IsScalarTower A K R] (x : R),
minpoly K x ∣ Polynomial.map (algebraMap A K) (minpoly A x)
The theorem `minpoly.dvd_map_of_isScalarTower` states that for any types `A`, `K` and `R` with `A` being a commutative ring, `K` being a field and `R` being a commutative ring, and given the algebra structures of `A` over `K`, `A` over `R`, and `K` over `R` and the fact that a scalar tower exists between `A`, `K`, and `R`. For any element `x` of `R`, the minimum polynomial of `x` over `K` divides the result of mapping the minimum polynomial of `x` over `A` through the algebra map from `A` to `K`. In other words, this theorem establishes a divisibility relationship between the minimum polynomial of `x` in different algebraic structures, under the mapping of those polynomials by the algebra map, when the algebraic structures form a scalar tower.
More concisely: Given a scalar tower of commutative rings `A` over `K` and `K` over `R`, and an element `x` of `R`, the minimum polynomial of `x` over `K` divides the minimum polynomial of `x` mapped through the algebra homomorphism from `A` to `K`.
|
minpoly.aeval_of_isScalarTower
theorem minpoly.aeval_of_isScalarTower :
∀ (R : Type u_3) {K : Type u_4} {T : Type u_5} {U : Type u_6} [inst : CommRing R] [inst_1 : Field K]
[inst_2 : CommRing T] [inst_3 : Algebra R K] [inst_4 : Algebra K T] [inst_5 : Algebra R T]
[inst_6 : IsScalarTower R K T] [inst_7 : CommSemiring U] [inst_8 : Algebra K U] [inst_9 : Algebra R U]
[inst_10 : IsScalarTower R K U] (x : T) (y : U),
(Polynomial.aeval y) (minpoly K x) = 0 → (Polynomial.aeval y) (minpoly R x) = 0
The theorem `minpoly.aeval_of_isScalarTower` states that if `y` is a conjugate of `x` over a field `K`, then it also is a conjugate over a subring `R`. More specifically, given types `R`, `K`, `T`, and `U` representing rings, a field, and algebraic structures respectively, along with algebra and scalar tower instances demonstrating their mathematical relationships, if `x` is in `T` and `y` is in `U`, and if `y` satisfies the minimal polynomial of `x` over `K` (which means `(Polynomial.aeval y) (minpoly K x) = 0`), then `y` also satisfies the minimal polynomial of `x` over `R` (which means `(Polynomial.aeval y) (minpoly R x) = 0`). The term "conjugate" here refers to roots of a polynomial - if `y` is a root of the minimal polynomial of `x` over one ring, it will be a root of the minimal polynomial over a subring.
More concisely: If `y` is a conjugate of `x` over a field `K`, then it is also a conjugate of `x` over any subring `R` containing `K`, and therefore satisfies the minimal polynomial of `x` over `R`.
|
minpoly.eq_of_irreducible_of_monic
theorem minpoly.eq_of_irreducible_of_monic :
∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B}
[inst_3 : Nontrivial B] {p : Polynomial A},
Irreducible p → (Polynomial.aeval x) p = 0 → p.Monic → p = minpoly A x
This theorem states that for types `A` and `B` where `A` is a field and `B` is a ring, and there exists an algebra from `A` to `B`, given a nontrivial element `x` of `B` and a polynomial `p` with coefficients from `A`, if the polynomial `p` is irreducible, `p` evaluated at `x` under the algebra homomorphism is zero, and `p` is a monic polynomial (its leading coefficient is 1), then `p` is equal to the minimal polynomial of `x` over `A`.
In simpler terms, a monic irreducible polynomial that zeroes out at some `x` under an algebra homomorphism is the minimal polynomial of that `x`.
More concisely: Given a field `A`, a ring `B` with an algebra homomorphism from `A` to `B`, a nontrivial `x` in `B`, and a monic irreducible polynomial `p` in `A[X]` such that `p(x) = 0`, then `p` is the minimal polynomial of `x` over `A`.
|
minpoly.prime
theorem minpoly.prime :
∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : IsDomain B] [inst_3 : Algebra A B]
{x : B}, IsIntegral A x → Prime (minpoly A x)
This theorem states that the minimal polynomial of an element is prime. More specifically, for any field `A` and ring `B` that is also an integral domain, with `A` acting as an algebra over `B`, and for any element `x` of `B` that is integral over `A`, the minimal polynomial of `x` over `A` is a prime element. Here, a prime element of a commutative monoid with zero (like a ring) is defined as an element that is not zero, not a unit, and if it divides the product of two elements, it must divide at least one of them.
More concisely: If `x` is an element integral over a field `A` in a ring `B` that is an integral domain, then the minimal polynomial of `x` over `A` is a prime element in `B`.
|
minpoly.ne_zero_of_finite
theorem minpoly.ne_zero_of_finite :
∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (e : B)
[inst_3 : FiniteDimensional A B], minpoly A e ≠ 0
This theorem states that for any type `A` which forms a field, and any type `B` which forms a ring and an algebra over `A`, if `B` is also a finite dimensional vector space over `A`, then the minimal polynomial of any element `e` of `B` over `A` is nonzero. In other words, if `B` is a finite-dimensional algebra over the field `A`, then the minimal polynomial of any element in `B` cannot be the zero polynomial.
More concisely: In a finite-dimensional algebra over a field, every non-zero element has a non-zero minimal polynomial.
|
minpoly_algHom_toLinearMap
theorem minpoly_algHom_toLinearMap :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CommRing L] [inst_2 : IsDomain L] [inst_3 : Algebra K L]
(σ : L →ₐ[K] L), IsOfFinOrder σ → minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1
This theorem states that for any field `K`, commutative ring `L`, such that `L` is a domain and an `K`-algebra, and for a given algebra homomorphism `σ : L →ₐ[K] L` that is of finite order, the minimal polynomial of `σ` over `K`, when viewed as a linear map, is `X ^ (orderOf σ) - 1`. Here, `X` represents the polynomial variable, `orderOf σ` is the order of the element `σ`, and `1` is the constant polynomial 1.
More concisely: For any field `K`, commutative ring `L` being a domain and `K`-algebra, if `σ : L → L` is a finite order algebra homomorphism, then the minimal polynomial of `σ` as a linear map over `K` is `X ^ (orderOf σ) - 1`.
|
minpoly.ker_aeval_eq_span_minpoly
theorem minpoly.ker_aeval_eq_span_minpoly :
∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B),
RingHom.ker (Polynomial.aeval x) = Submodule.span (Polynomial A) {minpoly A x}
This theorem, `minpoly.ker_aeval_eq_span_minpoly`, states that for any field `A`, ring `B`, algebra from `A` to `B`, and element `x` in `B`, the kernel of the ring homomorphism given by evaluating polynomials at `x` (which is defined by `Polynomial.aeval x`) is equal to the span of the minimal polynomial of `x` over `A` in the polynomial ring `Polynomial A`. In other words, the set of all polynomials which evaluate to zero at `x` is exactly the set of all scalar multiples of the minimal polynomial of `x` over `A`.
More concisely: The kernel of `Polynomial.aeval x` on the polynomial ring `Polynomial A` equals the span of the minimal polynomial of `x` over `A`.
|
minpoly.zero
theorem minpoly.zero :
∀ (A : Type u_1) (B : Type u_2) [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] [inst_3 : Nontrivial B],
minpoly A 0 = Polynomial.X
The theorem `minpoly.zero` states that for any types `A` and `B`, where `A` has a field structure, `B` has a ring structure, there is an algebra structure from `A` to `B`, and `B` is nontrivial, the minimal polynomial of `0` is `X`. In mathematical terms, this means that the minimal polynomial of the zero element from a field `A` to a nontrivial ring `B`, under a given algebra structure, is the polynomial with variable `X`.
More concisely: For any field `A` and nontrivial ring `B` with an algebra structure from `A` to `B`, the minimal polynomial of `0` in `B` (regarded as an `A`-module) is the constant polynomial `X`.
|
minpoly.dvd
theorem minpoly.dvd :
∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B)
{p : Polynomial A}, (Polynomial.aeval x) p = 0 → minpoly A x ∣ p
The theorem `minpoly.dvd` states that for any field `A`, ring `B`, algebra structure between `A` and `B`, and element `x` in `B`, if `x` is a root of a polynomial `p` over `A` (i.e., applying the algebra homomorphism from `A[X]` to `B` that sends `X` to `x` results in zero), then the minimal polynomial of `x` over `A` divides `p`. This result is also related to the theorem `minpoly.isIntegrallyClosed_dvd`, which has looser conditions on `A` but stricter ones on `B`.
More concisely: If `x` is a root of a polynomial `p` over field `A` in ring `B` with an algebra structure from `A`, then the minimal polynomial of `x` over `A` divides `p`.
|
minpoly.coeff_zero_eq_zero
theorem minpoly.coeff_zero_eq_zero :
∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : IsDomain B] [inst_3 : Algebra A B]
{x : B}, IsIntegral A x → ((minpoly A x).coeff 0 = 0 ↔ x = 0)
The theorem `minpoly.coeff_zero_eq_zero` states that for any algebra `B` over a field `A`, and for any element `x` in `B` that is integral over `A`, the constant coefficient (i.e., the coefficient of the zero-th degree term) of the minimal polynomial of `x` is zero if and only if `x` itself is zero. This theorem hinges on the concept of a minimal polynomial, which is a monic polynomial of the least degree that has `x` as a root, and the concept of an integral element, which is an element that is a root of some monic polynomial.
More concisely: For any element x integral over a field A in an algebra B, the constant coefficient of x's minimal polynomial equals 0 if and only if x is the zero element.
|
minpoly.one
theorem minpoly.one :
∀ (A : Type u_1) (B : Type u_2) [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] [inst_3 : Nontrivial B],
minpoly A 1 = Polynomial.X - 1
The theorem `minpoly.one` states that for any two types `A` and `B` where `A` is a field, `B` is a ring, there exists an algebra structure on `B` over `A`, and `B` is nontrivial, the minimal polynomial of `1` (the identity element of multiplication in `B`) is `X - 1`, where `X` is the polynomial variable or indeterminate. This polynomial is with coefficients in `A`. This essentially means that `1` is a root of the polynomial `X - 1`.
More concisely: For any field `A` and nontrivial ring `B` with an algebra structure over `A`, the minimal polynomial of `1` in `B` over `A` is `X - 1`.
|