IntermediateField.isSeparable_adjoin_pair_of_separable
theorem IntermediateField.isSeparable_adjoin_pair_of_separable :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x y : E},
(minpoly F x).Separable → (minpoly F y).Separable → IsSeparable F ↥F⟮x, y⟯
This theorem states that if `x` and `y` are both separable elements (meaning their minimal polynomials are separable), then the field extension generated by adjoining `x` and `y` to the base field `F` is also separable. As a result, any rational function of `x` and `y` is likewise a separable element. This theorem applies for any fields `F` and `E` where `F` is a subfield of `E`, and `x` and `y` are elements of `E`.
More concisely: If `F` is a field, `x` and `y` are separable elements in an extension field `E` of `F`, then `F(x, y)` is a separable extension of `F` and every rational function of `x` and `y` is a separable element in `E`.
|
Field.finSepDegree_eq_finrank_iff
theorem Field.finSepDegree_eq_finrank_iff :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : FiniteDimensional F E], Field.finSepDegree F E = FiniteDimensional.finrank F E ↔ IsSeparable F E
The theorem `Field.finSepDegree_eq_finrank_iff` states that for any field extension `E / F`, the separable degree of the extension is equal to its degree if and only if the extension is a separable extension, given that `E / F` is a finite extension. The separable degree is defined as the number of `F`-algebra homomorphisms from `E` to its algebraic closure, and the degree is essentially the dimension of `E` as a vector space over `F`. The term "separable extension" refers to a field extension where every element of the extended field is a root of a separable polynomial with coefficients in the base field.
More concisely: For a finite field extension E / F, the separable degree equals the degree if and only if E / F is separable.
|
Polynomial.Separable.natSepDegree_eq_natDegree
theorem Polynomial.Separable.natSepDegree_eq_natDegree :
∀ {F : Type u} [inst : Field F] {f : Polynomial F}, f.Separable → f.natSepDegree = f.natDegree
This theorem states that for any field `F` and any polynomial `f` of that field, if `f` is separable (i.e., it does not have any repeated roots), then the separable degree of `f` (`f.natSepDegree`) is equal to the natural degree of `f` (`f.natDegree`). This theorem also allows for the use of dot notation.
More concisely: If `F` is a field and `f` is a separable polynomial over `F`, then the separable degree and natural degree of `f` are equal. (`f.natSepDegree = f.natDegree`)
|
minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C
theorem minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
{x : E},
(minpoly F x).natSepDegree = 1 ↔
∃ n y, minpoly F x = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y)
This theorem states that for any field `F` and `E` with `E` being an algebra over `F` and a natural number `q` being the exponential characteristic of `F`, the minimal polynomial of an element `x` of `E / F` has a separable degree of one if and only if the minimal polynomial is of the form `Polynomial.expand F (q ^ n) (X - C y)` for some natural number `n` and a field element `y`.
Here, `Polynomial.expand F (q ^ n)` indicates the operation of expanding the polynomial by a factor of `q ^ n`, `Polynomial.X` represents the polynomial variable, and `Polynomial.C y` stands for the constant polynomial `y`. The minimal polynomial of an element `x` in `E / F` provides a polynomial with coefficients in `F` that `x` is a root of, and with the property that any other polynomial with `x` as a root has the minimal polynomial as a factor.
More concisely: For a field `F` with exponential characteristic `q`, and an algebra `E` over `F`, an element `x` of `E / F` has a separable minimal polynomial of degree one if and only if it is of the form `Polynomial.expand F (q ^ n) (X - C y)` for some natural number `n` and field element `y`.
|
Field.finSepDegree_eq_of_adjoin_splits
theorem Field.finSepDegree_eq_of_adjoin_splits :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K] {S : Set E},
IntermediateField.adjoin F S = ⊤ →
(∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) →
Field.finSepDegree F E = Nat.card (E →ₐ[F] K)
The theorem `Field.finSepDegree_eq_of_adjoin_splits` states that for any fields `F`, `E`, and `K`, with `F` and `E` having an algebra structure, and a set `S` of elements from `E`, if `E` is the field obtained by adjoining `F` with `S` (denoted as `E = F(S)`), and every element `s` of `S` is integral (or algebraic) over `F` and its minimal polynomial splits in `K`, then the separable degree of the field extension `E / F` (denoted as `Field.finSepDegree F E`), which is the number of `F`-algebra homomorphisms from `E` to the algebraic closure of `E` noted as a natural number, is equal to the cardinality of the set of all `F`-algebra homomorphisms from `E` to `K` (denoted as `Nat.card (E →ₐ[F] K)`). Note that the separable degree is defined to be zero if there are infinitely many such homomorphisms.
More concisely: If fields F, E, and K have an algebra structure, F is a subfield of E, S is a set of elements in E integral over F with splitting polynomials in K, then the separable degree of the field extension E/F equals the cardinality of the set of F-algebra homomorphisms from E to K.
|
Field.finSepDegree_eq_of_equiv
theorem Field.finSepDegree_eq_of_equiv :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K], (E ≃ₐ[F] K) → Field.finSepDegree F E = Field.finSepDegree F K
The theorem `Field.finSepDegree_eq_of_equiv` states that for any fields `F`, `E`, and `K` such that `F` is an algebra over `E` and `K`, if `E` and `K` are isomorphic as `F`-algebras, then they have the same finite separable degree over `F`. The finite separable degree of a field extension `E / F` is defined as the number of `F`-algebra homomorphisms from `E` to its algebraic closure, represented as a natural number, except when there are infinitely many of such homomorphisms, in which case it is defined to be zero.
More concisely: If fields `F`, `E`, and `K` are such that `F` is an algebra over `E` and `K`, and `E` and `K` are isomorphic as `F`-algebras, then they have the same finite separable degree over `F`.
|
Field.separable_add
theorem Field.separable_add :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x y : E},
(minpoly F x).Separable → (minpoly F y).Separable → (minpoly F (x + y)).Separable
This theorem states that in a field setting, if both `x` and `y` are separable elements (meaning the minimal polynomial of each element over a field F is separable), then their sum `x + y` is also a separable element. The theorem holds for any types `F` and `E` that form fields, and `F` is an algebra over `E`. Thus, separability is preserved under addition in this algebraic structure.
More concisely: In a field extension F/E, if x and y are separable elements over F, then x + y is also a separable element over F.
|
Polynomial.natSepDegree_eq_zero_iff
theorem Polynomial.natSepDegree_eq_zero_iff :
∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natSepDegree = 0 ↔ f.natDegree = 0
This theorem states that for any field `F` and a polynomial `f` with coefficients from `F`, the separable degree of the polynomial is zero if and only if the degree of the polynomial is zero. In other words, a polynomial will have a separable degree of zero precisely when it is a constant polynomial (i.e., its degree is zero).
More concisely: A polynomial over a field has separable degree zero if and only if its degree is zero.
|
Polynomial.natSepDegree_eq_of_isAlgClosed
theorem Polynomial.natSepDegree_eq_of_isAlgClosed :
∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (f : Polynomial F)
[inst_3 : IsAlgClosed E], f.natSepDegree = (f.aroots E).toFinset.card
The theorem `Polynomial.natSepDegree_eq_of_isAlgClosed` states that for any given field `F` and polynomial `f` with coefficients in `F`, and for any algebraically closed field `E` over `F`, the separable degree of `f` (which is defined as the number of distinct roots of `f` in its splitting field) is equal to the number of distinct roots of `f` in `E`. In other words, the separable degree of a polynomial is not dependent on the specific algebraically closed field chosen, and can be calculated by simply counting the distinct roots of the polynomial over any algebraically closed field.
More concisely: The separable degree of a polynomial over a field is equal to the number of its distinct roots in any algebraically closed extension.
|
Polynomial.Separable.comap_minpoly_of_isSeparable
theorem Polynomial.Separable.comap_minpoly_of_isSeparable :
∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w}
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K]
[inst_7 : IsSeparable F E] {x : K}, (minpoly E x).Separable → (minpoly F x).Separable
The theorem `Polynomial.Separable.comap_minpoly_of_isSeparable` states that if we have an extension tower `K / E / F` such that the extension `E / F` is separable, and if a value `x` from `K` is separable over `E`, then it will also be separable over `F`. Here, separability of a polynomial is defined as the polynomial being coprime with its derivative. The `minpoly E x` and `minpoly F x` represent the minimal polynomials of `x` over `E` and `F` respectively. So, if the minimal polynomial of `x` over `E` is separable, then the minimal polynomial of `x` over `F` is also separable.
More concisely: If `x` is separable over `E` in a separable extension tower `K / E / F`, then the minimal polynomial of `x` over `F` is coprime with its derivative, i.e., separable.
|
Polynomial.natSepDegree_expand
theorem Polynomial.natSepDegree_expand :
∀ {F : Type u} [inst : Field F] (f : Polynomial F) (q : ℕ) [hF : ExpChar F q] {n : ℕ},
((Polynomial.expand F (q ^ n)) f).natSepDegree = f.natSepDegree
The theorem `Polynomial.natSepDegree_expand` states that for any field `F` of exponential characteristic `q`, and for any polynomial `f` over `F`, if we expand `f` by a factor of `q^n` (where `n` is any natural number), the separable degree of the expanded polynomial is the same as the separable degree of the original polynomial. The separable degree of a polynomial is defined as the number of distinct roots it has over its splitting field. In other words, expansion by a factor of `q^n` does not change the number of unique roots of the polynomial.
More concisely: For any polynomial `f` over a field of characteristic `q`, the separable degree of `f` equals the separable degree of `f` expanded by a factor of `q^n`.
|
IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff
theorem IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
IsAlgebraic F α → (Field.finSepDegree F ↥F⟮α⟯ = FiniteDimensional.finrank F ↥F⟮α⟯ ↔ (minpoly F α).Separable)
This theorem states that for an element `α` of a field extension `E` over a field `F` that is algebraic over `F`, the separable degree of the field extension generated by `F` and `α` over `F` is equal to the degree of that same extension if and only if `α` is a separable element. In other words, the theorem connects the separability of an element `α` in a field extension with the coincidence of two specific measures of that extension - the separable degree and the degree (also known as the rank of the corresponding module).
More concisely: The separable degree and degree of a field extension generated by an algebraic element are equal if and only if the element is separable.
|
Polynomial.natSepDegree_le_natDegree
theorem Polynomial.natSepDegree_le_natDegree :
∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natSepDegree ≤ f.natDegree
This theorem states that for any given polynomial `f` over a field `F`, the separable degree of the polynomial is less than or equal to its degree. Here, the separable degree refers to the degree of the separable part of the polynomial. The separable part is the largest factor of the polynomial that has no repeated roots. This theorem basically says that a polynomial cannot have more distinct roots than its degree.
More concisely: The separable degree of a polynomial over a field is less than or equal to its degree.
|
Irreducible.natSepDegree_eq_one_iff_of_monic
theorem Irreducible.natSepDegree_eq_one_iff_of_monic :
∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [inst_1 : ExpChar F q],
f.Monic → Irreducible f → (f.natSepDegree = 1 ↔ ∃ n y, f = Polynomial.X ^ q ^ n - Polynomial.C y)
The theorem `Irreducible.natSepDegree_eq_one_iff_of_monic` states the following: Given a field `F` of exponential characteristic `q`, and a monic irreducible polynomial `f` over `F`, then the separable degree of `f` is one if and only if `f` can be written in the form `X ^ (q ^ n) - C y`, where `n` is a natural number and `y` is an element of `F`. Here, `X` represents the polynomial variable and `C y` represents a constant polynomial with coefficient `y`.
More concisely: A monic irreducible polynomial of degree n over a field of characteristic q is separable of degree 1 if and only if it can be expressed as X^(q^n) - C y, for some natural number n and constant polynomial C y over the field.
|
Polynomial.natSepDegree_ne_zero
theorem Polynomial.natSepDegree_ne_zero :
∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natDegree ≠ 0 → f.natSepDegree ≠ 0
This theorem states that for any field `F` and a polynomial `f` of type `Polynomial F`, if the natural degree of the polynomial `f` is non-zero, then the natural separable degree of the polynomial `f` is also non-zero. In other words, a non-constant polynomial (which is indicated by having a non-zero degree) will always have a non-zero separable degree.
More concisely: If `F` is a field and `f` is a non-constant polynomial over `F`, then the separable degree of `f` is non-zero.
|
IntermediateField.separable_of_mem_isSeparable
theorem IntermediateField.separable_of_mem_isSeparable :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : IntermediateField F E}
[inst_3 : IsSeparable F ↥L] {x : E}, x ∈ L → (minpoly F x).Separable
The theorem `IntermediateField.separable_of_mem_isSeparable` states that for any field `F` and `E` with `E` being an algebra over `F`, and given an intermediate field `L` which is separable over `F`, then for any element `x` that belongs to `L`, the minimal polynomial of `x` over `F` is a separable polynomial. Here, a separable polynomial is defined to be one that is coprime with its derivative.
More concisely: If `F` is a field, `E` is an algebra over `F`, `L` is a separable extension of `F`, and `x` is an element of `L`, then the minimal polynomial of `x` over `F` is separable.
|
Field.finSepDegree_eq_of_isAlgClosed
theorem Field.finSepDegree_eq_of_isAlgClosed :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K],
Algebra.IsAlgebraic F E → ∀ [inst_5 : IsAlgClosed K], Field.finSepDegree F E = Nat.card (E →ₐ[F] K)
The theorem states that, for any algebraic field extension `E / F` and any algebraically closed field `K / F`, the finite separable degree of `E / F` is equal to the cardinality, as a natural number, of the set of all `F`-algebra homomorphisms from `E` to `K`. Here, the finite separable degree of `E / F` is defined as the number of `F`-algebra homomorphisms from `E` to the algebraic closure of `E` as a natural number. However, if there are infinitely many such homomorphisms, it is defined to be zero.
More concisely: The theorem asserts that the finite separable degree of an algebraic field extension E/F equals the cardinality of the set of F-algebra homomorphisms from E to an algebraically closed field K over F.
|
minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C
theorem minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
{x : E}, (minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y
The theorem `minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C` asserts that for any fields `F` and `E` with `E` being an algebra over `F`, and for any element `x` of `E` with exponential characteristic `q`, the minimal polynomial of `x` over `F` has a separable degree of one if and only if the minimal polynomial can be expressed in the form of `X` raised to the power `q` raised to the power of some natural number `n`, minus a constant polynomial `y` from `F`. Here, `X` is the polynomial variable and `C y` represents the constant polynomial `y`.
More concisely: For any element `x` of an algebra `E` over field `F` with exponential characteristic `q`, the minimal polynomial of `x` over `F` has separable degree of one if and only if it can be written as `X^q^n - C`, where `X` is the polynomial variable, `C` is a constant from `F`, and `n` is a natural number.
|
IsSeparable.trans
theorem IsSeparable.trans :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K]
[inst_7 : IsSeparable F E] [inst_8 : IsSeparable E K], IsSeparable F K
This theorem states that if two field extensions `E / F` and `K / E` are both separable (i.e., for every element in the field extension, there exists a polynomial with coefficients in the smaller field such that the element is a root of the polynomial and the derivative of the polynomial is not zero), then the field extension `K / F` is also separable. This theorem is a statement about the transitivity of separability in field extensions and holds in the context of Algebra, where `F`, `E`, and `K` are fields and `F`, `E`, and `K` form a tower of fields (meaning `F` is a subfield of `E`, `E` is a subfield of `K`, and the algebra operations on `E` and `K` restrict to those on `F`).
More concisely: If field extensions `E/F` and `K/E` are both separable, then the composite extension `K/F` is separable.
|
Field.separable_inv
theorem Field.separable_inv :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (x : E),
(minpoly F x).Separable → (minpoly F x⁻¹).Separable
This theorem states that if `x` is a separable element over a field `F`, then its inverse `x⁻¹` is also a separable element over the same field. In the context of field theory, a separable element is one whose minimum polynomial over the field has distinct roots. Thus, the theorem establishes that the property of being separable is preserved under the operation of taking inverses.
More concisely: If `x` is a separable element over a field `F`, then `x⁻¹` is also a separable element over `F`.
|
IntermediateField.isSeparable_adjoin_simple_iff_separable
theorem IntermediateField.isSeparable_adjoin_simple_iff_separable :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
IsSeparable F ↥F⟮x⟯ ↔ (minpoly F x).Separable
This theorem states that for any two types `F` and `E` that are fields, with `F` being an algebra over `E`, and for any element `x` of `E`, the extension of `F` by `⟮x⟯` is separable if and only if the minimum polynomial of `x` over `F` is separable. As a result, any rational function of `x` is also a separable element.
More concisely: For any field extensions F of E, where F is an algebra over E and x is an element of E, the extension F.alg{x} is separable if and only if the minimum polynomial of x over F is separable, hence x and any rational function of x are separable elements.
|
Irreducible.natSepDegree_eq_one_iff_of_monic'
theorem Irreducible.natSepDegree_eq_one_iff_of_monic' :
∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [inst_1 : ExpChar F q],
f.Monic →
Irreducible f →
(f.natSepDegree = 1 ↔ ∃ n y, f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y))
This theorem states that for any field `F` with exponential characteristic `q`, and for any monic irreducible polynomial `f` over this field, the separable degree of `f` is one if and only if `f` can be expressed in the form `Polynomial.expand F (q ^ n) (Polynomial.X - Polynomial.C y)` for some natural number `n` and some element `y` of the field `F`. Here, `Polynomial.expand F (q ^ n)` represents the operation of expanding the polynomial by a factor of `q^n`, such that the sum `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`, and `Polynomial.X - Polynomial.C y` is a polynomial of the form `x - y` where `x` is the polynomial variable and `y` is a constant.
More concisely: For a monic irreducible polynomial `f` over a field `F` of characteristic `q`, the separable degree of `f` equals 1 if and only if `f` can be written as `Polynomial.expand F (q ^ n) (x - C y)` for some natural number `n` and constant `y` in `F`.
|
Polynomial.natSepDegree_eq_natDegree_of_separable
theorem Polynomial.natSepDegree_eq_natDegree_of_separable :
∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.Separable → f.natSepDegree = f.natDegree
This theorem states that for any given field `F` and a polynomial `f` of that field, if the polynomial `f` is separable, then the separable degree of the polynomial is equal to its degree. In other words, for a separable polynomial, the degree when considered as a separable polynomial, and the degree when considered just as a polynomial, are the same.
More concisely: For any separable polynomial `f` over a field `F`, the separable degree equals the degree of `f`.
|
Field.finSepDegree_dvd_finrank
theorem Field.finSepDegree_dvd_finrank :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
Field.finSepDegree F E ∣ FiniteDimensional.finrank F E
The theorem states that for any field extension `E / F`, the separable degree of the extension (as defined by `Field.finSepDegree`) is a divisor of the degree of the extension (as defined by `FiniteDimensional.finrank`). In other words, the number of `F`-algebra homomorphisms from `E` to its algebraic closure divides the rank (or dimension) of `E` as an `F`-vector space. This is an important property in field theory and algebraic geometry, connecting the algebraic structure of the extension with its geometric properties.
More concisely: The separable degree of a field extension divides its dimension as a vector space over the base field.
|
Polynomial.natSepDegree_X_sub_C
theorem Polynomial.natSepDegree_X_sub_C :
∀ {F : Type u} [inst : Field F] (x : F), (Polynomial.X - Polynomial.C x).natSepDegree = 1
The theorem `Polynomial.natSepDegree_X_sub_C` states that for any given field `F` and for any element `x` of this field, the separable degree of the polynomial `X - Cx` is equal to 1. Here, `X` is the polynomial variable and `Cx` is the constant polynomial `x`. The separable degree of a polynomial, denoted as `Polynomial.natSepDegree`, is defined as the number of distinct roots of the polynomial over its splitting field.
More concisely: The separable degree of the polynomial `X - Cx` over any field `F` is equal to 1 for any constant `C` in `F`.
|
Polynomial.HasSeparableContraction.natSepDegree_eq
theorem Polynomial.HasSeparableContraction.natSepDegree_eq :
∀ {F : Type u} [inst : Field F] {f : Polynomial F} {q : ℕ} [inst_1 : ExpChar F q]
(hf : Polynomial.HasSeparableContraction q f), f.natSepDegree = hf.degree
This theorem states that if a polynomial has a separable contraction, then its separable degree is equal to the degree of the given separable contraction. More precisely, for any field `F`, any polynomial `f` over `F`, and any natural number `q` which is assumed to be the exponential characteristic of `F`, if `f` has a separable contraction of degree `q`, then the separable degree of `f` is equal to the degree of this separable contraction.
More concisely: If a polynomial `f` over a field `F` of exponential characteristic `q` has a separable contraction of degree `q`, then the separable degree of `f` equals the degree of this contraction.
|
Irreducible.natSepDegree_dvd_natDegree
theorem Irreducible.natSepDegree_dvd_natDegree :
∀ {F : Type u} [inst : Field F] {f : Polynomial F}, Irreducible f → f.natSepDegree ∣ f.natDegree
This theorem states that for any given field `F` and any irreducible polynomial `f` of that field, the separable degree (`natSepDegree`) of the polynomial `f` is a divisor of the degree (`natDegree`) of the polynomial `f`. In mathematical terms, for an irreducible polynomial, its separable degree always divides its degree.
More concisely: For any irreducible polynomial over a field, its separable degree divides its degree.
|
Polynomial.natSepDegree_eq_zero
theorem Polynomial.natSepDegree_eq_zero :
∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natDegree = 0 → f.natSepDegree = 0
This theorem states that for any field `F` and for any polynomial `f` of that field, if the natural degree of the polynomial is zero (i.e., the polynomial is a constant), then the separable degree of the polynomial is also zero. This theorem essentially conveys that a constant polynomial cannot have a non-zero separable degree.
More concisely: For any field `F` and polynomial `f` over `F` of degree zero, the separable degree of `f` is zero.
|
minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow
theorem minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
{x : E},
(minpoly F x).natSepDegree = 1 ↔
∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n
This theorem states that for any field `F`, field `E`, algebra from `F` to `E`, and a natural number `q` representing the exponential characteristic of the field `F`, and for any element `x` of `E`, the minimal polynomial of `x` over `F` has a separable degree of one if and only if there exists a natural number `n` such that the minimal polynomial, when mapped from `F` to `E` using the algebra map, is equal to the polynomial `(X - x) ^ (q ^ n)`. Here `X` represents a polynomial indeterminate and `Polynomial.C x` represents the constant polynomial `x`. The term 'separable degree' refers to the degree of the separable part of a polynomial, which is a concept in field theory and algebraic number theory.
More concisely: For any field `F`, field `E`, algebra `α : Algebra F E`, natural number `q` (exponential characteristic of `F`), and `x ∈ E`, the minimal polynomial of `x` over `F` is of separable degree one if and only if it equals `(X - α ℛ x) ^ (q ^ n)` for some natural number `n`.
|
Polynomial.natSepDegree_eq_natDegree_iff
theorem Polynomial.natSepDegree_eq_natDegree_iff :
∀ {F : Type u} [inst : Field F] (f : Polynomial F), f ≠ 0 → (f.natSepDegree = f.natDegree ↔ f.Separable)
This theorem states that for any non-zero polynomial `f` in a field `F`, the separable degree of `f` is equal to its degree if and only if `f` is a separable polynomial. In other words, the separable degree of a non-zero polynomial exactly matches its degree when the polynomial is separable.
More concisely: The separable degree of a non-zero polynomial over a field equals its degree if and only if the polynomial is separable.
|
Field.finSepDegree_le_finrank
theorem Field.finSepDegree_le_finrank :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : FiniteDimensional F E], Field.finSepDegree F E ≤ FiniteDimensional.finrank F E
The theorem `Field.finSepDegree_le_finrank` states that for any finite algebraic extension `E / F` of fields, the separable degree of the extension is less than or equal to the degree of the extension. Here, the separable degree of `E / F` is defined as the number of `F`-algebra homomorphisms from `E` to its algebraic closure and the degree of `E / F` corresponds to the rank of the module formed by `E` over `F`, when considered as a vector space over `F`. The theorem essentially compares the complexity of the extension when considering separability versus when considering it purely as a vector space.
More concisely: The separable degree of a finite algebraic extension of fields is less than or equal to its degree as a vector space over the base field.
|
Polynomial.natSepDegree_ne_zero_iff
theorem Polynomial.natSepDegree_ne_zero_iff :
∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natSepDegree ≠ 0 ↔ f.natDegree ≠ 0
This theorem states that for any field F and a polynomial f over F, the separable degree of the polynomial is non-zero if and only if the natural degree of the polynomial is non-zero. In other words, a polynomial has a non-zero separable degree exactly when it is a non-constant polynomial.
More concisely: The separable degree of a polynomial over a field is non-zero if and only if its natural degree is non-zero. (Equivalently, a polynomial is separable if and only if it is non-constant.)
|
Field.separable_mul
theorem Field.separable_mul :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x y : E},
(minpoly F x).Separable → (minpoly F y).Separable → (minpoly F (x * y)).Separable
This theorem states that, given any fields `F` and `E` where `E` is an algebra over `F`, and any two elements `x` and `y` in `E` that are separable over `F`, the product `x * y` is also separable over `F`. Here, an element being separable means that its minimal polynomial over `F` is separable, i.e., has distinct roots.
More concisely: If fields `F` and `E` are given with `E` an algebra over `F`, and `x` and `y` are separable elements in `E` over `F`, then `x * y` is also separable over `F`.
|
IntermediateField.finSepDegree_adjoin_simple_le_finrank
theorem IntermediateField.finSepDegree_adjoin_simple_le_finrank :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
IsAlgebraic F α → Field.finSepDegree F ↥F⟮α⟯ ≤ FiniteDimensional.finrank F ↥F⟮α⟯
This theorem states that if an element `α` is algebraic over a field `F` in an algebraic extension `F⟮α⟯ / F`, then the separable degree of `F⟮α⟯ / F` is less than or equal to the degree of `F⟮α⟯ / F`. Here, the separable degree of `F⟮α⟯ / F` is defined as the number of `F`-algebra homomorphisms from `F⟮α⟯` to the algebraic closure of `F⟮α⟯`, and the degree of `F⟮α⟯ / F` is the rank of the module `F⟮α⟯` over `F`. This theorem is relevant in the context of algebraic number theory and field theory.
More concisely: The separable degree of an algebraic extension of a field by an algebraic element is less than or equal to its degree.
|
IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree
theorem IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {α : E},
IsAlgebraic F α → Field.finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree
This theorem states that for any field `F` and `E`, where `E` is an algebraic extension of `F`, and for any element `α` in `E` that is algebraic over `F`, the separable degree of the field `F` adjoined with `α` over `F` is equal to the separable degree of the minimal polynomial of `α` over `F`. The separable degree of a field extension is the number of homomorphisms from the extension field to its algebraic closure, represented as a natural number, or zero if there are infinitely many. The minimal polynomial of a number over a field is the simplest polynomial with coefficients in the field that has the number as a root.
More concisely: For any field `F` and algebraic extension `E/F`, and for any algebraic element `α` in `E`, the separable degree of `F(α)/F` equals the degree of the minimal polynomial of `α` over `F`.
|
Polynomial.natSepDegree_eq_of_splits
theorem Polynomial.natSepDegree_eq_of_splits :
∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (f : Polynomial F),
Polynomial.Splits (algebraMap F E) f → f.natSepDegree = (f.aroots E).toFinset.card
The theorem `Polynomial.natSepDegree_eq_of_splits` states that for any given polynomial `f` and fields `F` and `E` with an algebraic structure between them, if the polynomial `f` splits over `E` (meaning the polynomial is either zero or all of its irreducible factors have degree 1 when mapped to `E`), then the separable degree of the polynomial is equal to the number of distinct roots that the polynomial has over `E`. In mathematical terms, if a polynomial `f` over a field `F` splits over an extension field `E`, then the separable degree of `f` is equal to the cardinality of the set of `f`'s distinct roots in `E`.
More concisely: If a polynomial over a field splits in an extension field, then its separable degree equals the number of distinct roots in that extension field.
|
Polynomial.IsSeparableContraction.natSepDegree_eq
theorem Polynomial.IsSeparableContraction.natSepDegree_eq :
∀ {F : Type u} [inst : Field F] {f g : Polynomial F} {q : ℕ} [inst_1 : ExpChar F q],
Polynomial.IsSeparableContraction q f g → f.natSepDegree = g.natDegree
The theorem `Polynomial.IsSeparableContraction.natSepDegree_eq` states that for any field `F`, and for any two polynomials `f` and `g` over this field, if `g` is a separable contraction of `f` with respect to a given exponent `q`, then the separable degree of `f` is equal to the degree of `g`. In other words, if a polynomial `g` is a contraction of `f` in a way that `g` remains separable, and the operation of contraction is such that `g(x^(q^m)) = f(x)` for some natural number `m`, then the separable degree of `f` is exactly the degree of `g`.
More concisely: For any field `F` and polynomials `f` and `g` over `F` with `g` a separable contraction of `f` with degree `g.deg` and some `q` such that `g(x^(q^m)) = f(x)` for some natural number `m`, it holds that `deg(f) = deg(g)`.
|
Field.finSepDegree_eq_finrank_of_isSeparable
theorem Field.finSepDegree_eq_finrank_of_isSeparable :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [inst_3 : IsSeparable F E],
Field.finSepDegree F E = FiniteDimensional.finrank F E
This theorem states that for a separable extension `E / F`, its separable degree is equal to its degree. This is to say, the number of `F`-algebra homomorphisms from `E` to the algebraic closure of `E`, represented as a natural number (or zero if there are infinitely many), is equal to the rank of the module `E` over the field `F`, represented as a natural number. However, in the case of an infinite extension `E / F` which means that there are infinitely many `F`-algebra homomorphisms, the cardinality of these homomorphisms is not generally equal to the rank of the module.
More concisely: The separable degree of a separable extension equals its degree as the number of its separable algebra homomorphisms to the algebraic closure, which is equal to the rank of the extension as a module over the base field.
|
Field.finSepDegree_mul_finSepDegree_of_isAlgebraic
theorem Field.finSepDegree_mul_finSepDegree_of_isAlgebraic :
∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w)
[inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
Algebra.IsAlgebraic E K → Field.finSepDegree F E * Field.finSepDegree E K = Field.finSepDegree F K
The theorem `Field.finSepDegree_mul_finSepDegree_of_isAlgebraic` states that given a tower of field extensions `K / E / F`, where `K / E` is an algebraic extension, the separable degrees of the extensions satisfy the tower law. Specifically, the separable degree of `E` over `F` multiplied by the separable degree of `K` over `E` equals the separable degree of `K` over `F`. This is analogous to the multiplication rule for the ranks of finite-dimensional vector spaces.
More concisely: The separable degrees of the field extensions in a tower `K / E / F` satisfy the multiplicative property, where `K / E` is algebraic and `K / F` is the composition of `K / E` and `E / F`.
|
Field.separable_algebraMap
theorem Field.separable_algebraMap :
∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (x : F),
(minpoly F ((algebraMap F E) x)).Separable
This theorem states that for any field `F` (of type `F`), and any field `E` (of type `E`), with `F` being an algebra over `E`, any element `x` of `F` is a separable element when it is embedded into `E` using the algebra map. In other words, the minimal polynomial of the element `x` under the algebra map from `F` to `E` is separable. Here, a polynomial is said to be separable if it has no multiple roots.
More concisely: For any field extension `F` over `E` (with `F` being an algebra over `E`), every element `x` in `F` is separably embedded if and only if the minimal polynomial of `x` over `E` is separable.
|