minpoly.min
theorem minpoly.min :
∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B)
{p : Polynomial A}, p.Monic → (Polynomial.aeval x) p = 0 → (minpoly A x).degree ≤ p.degree
This theorem states that for any types `A` and `B`, with `A` being a commutative ring, `B` being a ring, and `B` being an `A`-algebra, for any element `x` of type `B`, and any monic polynomial `p` over `A`, if `x` is a root of `p` (i.e., `p(x) = 0`), then the degree of the minimal polynomial of `x` is less than or equal to the degree of `p`. In other words, the minimal polynomial of `x` is the monic polynomial of smallest degree that has `x` as its root.
More concisely: For any commutative ring `A`, ring `B` being an `A`-algebra, monic polynomial `p` over `A`, and element `x` in `B` such that `p(x) = 0`, the degree of the minimal polynomial of `x` is less than or equal to the degree of `p`.
|
minpoly.ne_zero
theorem minpoly.ne_zero :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B}
[inst_3 : Nontrivial A], IsIntegral A x → minpoly A x ≠ 0
The theorem `minpoly.ne_zero` states that for any algebra `B` over a commutative ring `A` (both `A` and `B` are types), and for any element `x` of `B`, if `A` is nontrivial and `x` is integral over `A`, then the minimal polynomial of `x` over `A` is not zero. Here, an element being integral means that it is a root of some monic polynomial with coefficients in `A`, and a nontrivial ring means a ring with at least two distinct elements.
More concisely: If `A` is a nontrivial commutative ring and `x` is an element integral over `A` in the algebra `B` over `A`, then the minimal polynomial of `x` over `A` is non-zero.
|
minpoly.unique'
theorem minpoly.unique' :
∀ (A : Type u_1) {B : Type u_2} [inst : CommRing 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.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0) → p = minpoly A x
This theorem, referred to as `minpoly.unique'`, states that for any commutative ring `A`, ring `B`, algebra from `A` to `B`, and element `x` of `B`, given a polynomial `p` over `A` that is monic (i.e., its leading coefficient is 1) and such that the application of `x` to `p` through algebra homomorphism (denoted by `Polynomial.aeval x`) equals 0, if for all polynomials `q` over `A` with a degree less than the degree of `p`, `q` equals 0 or the application of `x` to `q` through algebra homomorphism is non-zero, then `p` is equal to the minimal polynomial of `x` over `A`.
In other words, a monic polynomial `p` that evaluates to 0 when applied with `x` and dominates all other such polynomials in terms of degree, is the minimal polynomial of `x` over `A`.
More concisely: If `A` is a commutative ring, `B` is a ring, `Algebra A B` is an algebra from `A` to `B`, `x` is an element of `B`, `p` is a monic polynomial over `A` such that `Polynomial.aeval x p = 0` and `Polynomial.aeval x q = 0` implies `deg q < deg p` or `q = 0`, then `p` is the minimal polynomial of `x` over `A`.
|
minpoly.ne_one
theorem minpoly.ne_one :
∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B)
[inst_3 : Nontrivial B], minpoly A x ≠ 1
This theorem states that for any types `A` and `B`, where `A` is a commutative ring and `B` is a ring with an algebraic structure over `A`, the minimal polynomial of any element `x` of `B`, under the prerequisite that `B` is nontrivial, is not equal to `1`. Here, a nontrivial ring is a ring that has more than one distinct element.
More concisely: For any commutative ring `A` and a ring `B` with an algebraic structure over `A` that is nontrivial, the minimal polynomial of any element in `B` is not equal to the constant polynomial `1`.
|
minpoly.monic
theorem minpoly.monic :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B},
IsIntegral A x → (minpoly A x).Monic
The theorem `minpoly.monic` states that for any types `A` and `B`, where `A` is a commutative ring, `B` is a ring, and there exists an algebra structure over `B` with `A`, then for any element `x` of `B` that is integral over `A`, the minimal polynomial of `x` over `A` is monic. In other words, the leading coefficient of the minimal polynomial of an integral element is 1.
More concisely: If `x` is an integral element over a commutative ring `A` in a ring `B` with an algebra structure over `A`, then the minimal polynomial of `x` over `A` is monic (i.e., its leading coefficient is 1).
|
minpoly.algEquiv_eq
theorem minpoly.algEquiv_eq :
∀ {A : Type u_1} {B : Type u_2} {B' : Type u_3} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Ring B']
[inst_3 : Algebra A B] [inst_4 : Algebra A B'] (f : B ≃ₐ[A] B') (x : B), minpoly A (f x) = minpoly A x
This theorem states that for any types `A`, `B`, and `B'`, where `A` is a commutative ring and `B` and `B'` are rings, and we have algebra structures from `A` to `B` and `A` to `B'`, if `f` is an algebraic equivalence from `B` to `B'` and `x` is an element in `B`, then the minimal polynomial of `f(x)` over `A` is equal to the minimal polynomial of `x` over `A`. This means that the algebraic equivalence `f` preserves the minimal polynomial of any element.
More concisely: For any commutative ring `A`, and rings `B`, `B'` with `A`-algebra structures, if `f: B -> B'` is an algebraic equivalence and `x` is an element in `B`, then the minimal polynomial of `f(x)` over `A` equals the minimal polynomial of `x` over `A`.
|
minpoly.algebraMap_eq
theorem minpoly.algebraMap_eq :
∀ {A : Type u_1} {B' : Type u_3} [inst : CommRing A] [inst_1 : Ring B'] [inst_2 : Algebra A B'] {B : Type u_4}
[inst_3 : CommRing B] [inst_4 : Algebra A B] [inst_5 : Algebra B B'] [inst_6 : IsScalarTower A B B'],
Function.Injective ⇑(algebraMap B B') → ∀ (x : B), minpoly A ((algebraMap B B') x) = minpoly A x
This theorem, `minpoly.algebraMap_eq`, states that for any types `A`, `B'` and `B`, where `A` and `B` have a commutative ring structure and `B'` has a ring structure, and where `A`, `B` and `B'` have an algebra structure, with `B` and `B'` forming a scalar tower over `A`, if the algebra map from `B` to `B'` is injective, then for any element `x` of `B`, the minimum polynomial of `x` under the algebra map from `B` to `B'` is equal to the minimum polynomial of `x` in `A`.
In more simple terms, if we have two algebraic structures over a common base and a "nice" way (the injective algebra map) to go from one to the other, then the minimum polynomial of an element in the first structure is the same whether we consider it as an element of the first structure or map it to the second one.
More concisely: If `A`, `B`, and `B'` are commutative rings with algebra structures over a common base, `B` and `B'` form a scalar tower over `A`, and the algebra map from `B` to `B'` is injective, then the minimum polynomial of any element in `B` under the algebra map is equal to its minimum polynomial in `A`.
|
minpoly.eq_X_sub_C_of_algebraMap_inj
theorem minpoly.eq_X_sub_C_of_algebraMap_inj :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (a : A),
Function.Injective ⇑(algebraMap A B) → minpoly A ((algebraMap A B) a) = Polynomial.X - Polynomial.C a
The theorem, `minpoly.eq_X_sub_C_of_algebraMap_inj`, states that if we have an injective ring extension from `A` to `B` (denoted `B/A`), and `a` is an element of `A`, then the minimal polynomial of the image of `a` under the algebra map from `A` to `B` is `X - C a`. Here, `X` represents the polynomial variable and `C a` represents the constant polynomial `a`. In other words, the minimal polynomial of the element `a` in `B`, when `B` is viewed as an algebra over `A`, is the simple polynomial `X - a`, provided that the mapping from `A` to `B` is injective.
More concisely: If `A` injects into `B`, then the minimal polynomial of `a` in `B` as an `A`-algebra is `X - a`.
|
minpoly.aeval
theorem minpoly.aeval :
∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B),
(Polynomial.aeval x) (minpoly A x) = 0
This theorem states that for any given type `A` with a commutative ring structure, type `B` with a ring structure and `B` being an `A`-algebra, any element `x` of type `B` is a root of its minimal polynomial. In other words, if we evaluate the minimal polynomial of `x` at `x` using the `Polynomial.aeval` function, the result is zero. In mathematical terms, it is equivalent to saying that if $p(x)$ represents the minimal polynomial of $x$, then $p(x) = 0$.
More concisely: For any commutative ring `A`, `A`-algebra `B` with an element `x`, the minimal polynomial of `x` in `B[X]` evaluates to zero at `x`.
|
minpoly.natDegree_pos
theorem minpoly.natDegree_pos :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B}
[inst_3 : Nontrivial B], IsIntegral A x → 0 < (minpoly A x).natDegree
The theorem `minpoly.natDegree_pos` states that for any commutative ring `A`, any ring `B`, and any algebra `A B`, if `x` is an element of `B` that is integral over `A`, and `B` is nontrivial, then the natural degree of the minimal polynomial of `x` over `A` is positive. In simpler terms, the minimal polynomial of an algebraic element over a ring has a non-zero degree.
More concisely: The minimal polynomial of any algebraic element over a nontrivial ring has positive degree.
|
minpoly.degree_pos
theorem minpoly.degree_pos :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B}
[inst_3 : Nontrivial B], IsIntegral A x → 0 < (minpoly A x).degree
This theorem states that, given a commutative ring `A`, a ring `B`, and an algebra structure of `B` over `A`, if `x` is an element of `B` which is integral over `A`, and `B` is nontrivial (i.e., not equal to the zero ring), then the degree of the minimal polynomial of `x` over `A` is positive. In other words, any element that is integral over a commutative ring within a nontrivial ring has a minimal polynomial with a degree greater than zero.
More concisely: If `A` is a commutative ring, `B` is a nontrivial `A`-algebra, and `x` is an integral element of `B` over `A`, then the minimal polynomial of `x` over `A` has positive degree.
|
minpoly.irreducible
theorem minpoly.irreducible :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B}
[inst_3 : IsDomain A] [inst_4 : IsDomain B], IsIntegral A x → Irreducible (minpoly A x)
The theorem `minpoly.irreducible` states that for any commutative ring `A`, any ring `B`, and any element `x` in `B`, if `A` and `B` are integral domains and `x` is integral over `A`, then the minimal polynomial of `x` over `A` is irreducible. In other words, the minimal polynomial cannot be factored into two non-constant polynomials. This is an important property in the theory of field extensions, ensuring that minimal polynomials have a unique factorization, similar to prime numbers in the integers.
More concisely: Given commutative integral domains A and B, and an element x in B integral over A, the minimal polynomial of x over A is irreducible.
|
minpoly.algHom_eq
theorem minpoly.algHom_eq :
∀ {A : Type u_1} {B : Type u_2} {B' : Type u_3} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Ring B']
[inst_3 : Algebra A B] [inst_4 : Algebra A B'] (f : B →ₐ[A] B'),
Function.Injective ⇑f → ∀ (x : B), minpoly A (f x) = minpoly A x
The theorem `minpoly.algHom_eq` states that for any types `A`, `B`, and `B'`, where `A` is a commutative ring, `B` and `B'` are rings, and algebra structures exist from `A` to `B` and `A` to `B'`, and for any algebra homomorphism `f` from `B` to `B'` over `A`, if the homomorphism `f` is injective, then for all `x` in `B`, the minimal polynomial of `f(x)` over `A` is the same as the minimal polynomial of `x` over `A`. In other words, an injective algebra homomorphism does not change the minimal polynomial of an element in the domain ring when we view these polynomials over a common commutative ring.
More concisely: If `f` is an injective algebra homomorphism from `B` to `B'` over a commutative ring `A`, then for all `x` in `B`, the minimal polynomial of `f(x)` over `A` equals the minimal polynomial of `x` over `A`.
|
minpoly.eq_zero
theorem minpoly.eq_zero :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B},
¬IsIntegral A x → minpoly A x = 0
The theorem `minpoly.eq_zero` is stating that for all types `A` and `B`, where `A` is a commutative ring and `B` is a ring, and there is an algebraic structure from `A` to `B`, then for any element `x` of `B`, if `x` is not integral over `A` -- that is, `x` is not a root of any monic polynomial with coefficients in `A` -- then the minimal polynomial of `x` over `A` is the zero polynomial.
More concisely: If `x` is an element of a ring `B` that is not integral over a commutative ring `A`, then the minimal polynomial of `x` over `A` is the zero polynomial.
|
minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly
theorem minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly :
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B}
{a : Polynomial A}, IsIntegral A x → a.Monic → DvdNotUnit a (minpoly A x) → (Polynomial.aeval x) a ≠ 0
The theorem `minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly` states that if a monic polynomial `a` strictly divides the minimal polynomial of an element `x` of an algebra `B` over a commutative ring `A`, then `x` cannot be a root of `a`. Here, the element `x` is integral over `A`, and "strictly divides" means that the result of division of the minimal polynomial by `a` is not a unit. This theorem essentially tells us about a certain restriction on the possible roots of the polynomial `a`.
More concisely: If a monic polynomial `a` strictly divides the minimal polynomial of an integral element `x` in algebra `B` over commutative ring `A`, then `x` is not a root of `a`.
|
minpoly.not_isUnit
theorem minpoly.not_isUnit :
∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B)
[inst_3 : Nontrivial B], ¬IsUnit (minpoly A x)
The theorem `minpoly.not_isUnit` states that for any given types `A` and `B`, where `A` is a commutative ring, `B` is a ring, and `B` is an algebra over `A`, and for any element `x` of type `B` where `B` is nontrivial, the minimal polynomial of `x` over `A` cannot be a unit. In other words, there doesn't exist an element in the ring of polynomials over `A` that is a multiplicative inverse of the minimal polynomial of `x`.
More concisely: For any commutative ring `A`, ring `B` that is an algebra over `A` with a nontrivial element `x`, the minimal polynomial of `x` over `A` is not a unit in the ring of polynomials over `A`.
|