Polynomial.Separable.map_minpoly
theorem Polynomial.Separable.map_minpoly :
∀ {A : Type u_1} [inst : CommRing A] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra A K] {R : Type u_3}
[inst_3 : CommRing R] [inst_4 : Algebra A R] [inst_5 : Algebra K R] [inst_6 : IsScalarTower A K R] {x : R},
(minpoly A x).Separable → (minpoly K x).Separable
The theorem `Polynomial.Separable.map_minpoly` states that if you have an extension tower `R / K / A`, where `R`, `K` and `A` are types with necessary algebraic structure (`A` and `R` are commutative rings, `K` is a field, and there are algebra instances from `A` to `K`, `K` to `R`, and `A` to `R`, along with a scalar tower structure), then a polynomial `x` which is of type `R` and is separable over `A` is also separable over `K`. In this context, a polynomial is said to be separable if it is coprime with its derivative.
More concisely: If `R` is a commutative ring, `K` is a field, `A` is a commutative ring with an algebra structure over `R`, `K` and `A`, and `x` is a separable polynomial of degree `n` over `A`, then `x` is also separable over `K` if and only if `x` and its derivative `dx/dx` have no common roots in `K`.
|
Irreducible.separable
theorem Irreducible.separable :
∀ {F : Type u} [inst : Field F] [inst_1 : CharZero F] {f : Polynomial F}, Irreducible f → f.Separable
This theorem states that for any field `F` with characteristic zero, any irreducible polynomial `f` over `F` is separable. In other words, the polynomial `f` and its derivative are coprime. Here, a polynomial is said to be separable if it is coprime with its derivative, and a field is said to have characteristic zero if its characteristic, which is the smallest positive integer such that multiplication by it results in zero, is zero. Note that an irreducible polynomial is a non-constant polynomial that cannot be factored into the product of two non-constant polynomials.
More concisely: In a field of characteristic zero, every irreducible polynomial is separable, meaning it is coprime with its derivative.
|
Polynomial.nodup_roots_iff_of_splits
theorem Polynomial.nodup_roots_iff_of_splits :
∀ {F : Type u} [inst : Field F] {f : Polynomial F},
f ≠ 0 → Polynomial.Splits (RingHom.id F) f → (f.roots.Nodup ↔ f.Separable)
This theorem states that for any given non-zero polynomial `f` over a field `F`, if `f` splits, then it has no repeated roots in the field `F` if and only if it is separable. Here, a polynomial is said to split if it is either zero or all of its irreducible factors have degree 1. A polynomial is separable if it has no repeated roots. The term `RingHom.id F` refers to the identity ring homomorphism from the field `F` to itself.
More concisely: A non-zero polynomial over a field splits and has no repeated roots if and only if it is separable.
|
Polynomial.Separable.isIntegral
theorem Polynomial.Separable.isIntegral :
∀ {F : Type u_1} {K : Type u_2} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] {x : K},
(minpoly F x).Separable → IsIntegral F x
The theorem states that if `x` is an element of a ring `K` over a commutative ring `F`, and the minimal polynomial of `x` over `F` is separable, then `x` is integral over `F`. This is because the minimal polynomial of a non-integral element is `0`, which is not separable. In mathematical terms, a polynomial is considered separable if it is coprime with its derivative, and an element `x` of an algebra `A` over a commutative ring `R` is termed integral if it is a root of some monic polynomial `p : R[X]`.
More concisely: If `x` is an element of a ring `K` over a commutative ring `F`, and the minimal polynomial of `x` over `F` is separable and non-zero, then `x` is integral over `F`.
|
Polynomial.nodup_aroots_iff_of_splits
theorem Polynomial.nodup_aroots_iff_of_splits :
∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra F K] {f : Polynomial F},
f ≠ 0 → Polynomial.Splits (algebraMap F K) f → ((f.aroots K).Nodup ↔ f.Separable)
The theorem `Polynomial.nodup_aroots_iff_of_splits` states that for any field `F`, field `K`, and polynomial `f` over `F`, if `f` is non-zero and splits in `K`, then `f` has no repeated roots in `K` if and only if it is separable. Here 'splits' means that the polynomial is either zero or all of its irreducible factors have degree 1, and 'separable' relates to a property of polynomials which have distinct roots. The `algebraMap F K` represents an embedding from `F` to `K`. The `.Nodup` function checks if `f` has no duplicate roots in `K`. In essence, this theorem connects two concepts of polynomials: having no repeated roots and separability, under the condition of splitting in a field extension.
More concisely: For a non-zero polynomial `f` over field `F`, `f` has no repeated roots in a field extension `K` if and only if `f` splits in `K` and is separable.
|
IsSeparable.isAlgebraic
theorem IsSeparable.isAlgebraic :
∀ (F : Type u_1) (K : Type u_2) [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] [inst_3 : Nontrivial F]
[inst_4 : IsSeparable F K], Algebra.IsAlgebraic F K
The theorem `IsSeparable.isAlgebraic` states that for any two types `F` and `K`, where `F` is a commutative ring, `K` is a ring, and `K` is an algebra over `F`, if `F` is nontrivial and `K` is separable over `F`, then every element of `K` is algebraic over `F`. In other words, if `K` is a separable algebra over a nontrivial commutative ring `F`, then all elements of `K` can be expressed as roots of some non-zero polynomial with coefficients in `F`.
More concisely: If `F` is a nontrivial commutative ring and `K` is a separable algebra over `F`, then every element of `K` is algebraic over `F`.
|
Associated.separable
theorem Associated.separable :
∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, Associated f g → f.Separable → g.Separable
The theorem `Associated.separable` states that for any commutative semiring `R` and any two polynomials `f` and `g` over `R`, if `f` and `g` are associated (i.e., one can be obtained from the other by multiplying by a unit on the right), and if `f` is a separable polynomial (which means it is coprime with its derivative), then `g` is also a separable polynomial.
More concisely: If `f` and `g` are associated polynomials over a commutative semiring, and `f` is separable, then `g` is also separable.
|
Polynomial.Separable.of_dvd
theorem Polynomial.Separable.of_dvd :
∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, f.Separable → g ∣ f → g.Separable
The theorem `Polynomial.Separable.of_dvd` states that for any commutative semiring `R` and any two polynomials `f` and `g` over `R`, if `f` is a separable polynomial and `g` divides `f`, then `g` is also a separable polynomial. Here, a polynomial is considered separable if it is coprime with its derivative, i.e., the polynomial and its derivative share no common factor other than 1.
More concisely: If `f` is a separable polynomial over a commutative semiring `R` and `g` is a divisor of `f`, then `g` is also a separable polynomial.
|
Polynomial.Separable.map
theorem Polynomial.Separable.map :
∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] {p : Polynomial R},
p.Separable → ∀ {f : R →+* S}, (Polynomial.map f p).Separable
The theorem `Polynomial.Separable.map` states that for any commutative semirings `R` and `S`, any polynomial `p` from `R`, and any ring homomorphism `f` from `R` to `S`, if the polynomial `p` is separable over `R`, then the mapped polynomial `Polynomial.map f p` is also separable over `S`. Here, a polynomial is considered separable if it is coprime with its derivative.
More concisely: If `p` is a separable polynomial over a commutative semiring `R`, then `Polynomial.map f p` is a separable polynomial over the image semiring `f(R)` under a ring homomorphism `f`.
|
Polynomial.X_pow_sub_one_separable_iff
theorem Polynomial.X_pow_sub_one_separable_iff :
∀ {F : Type u} [inst : Field F] {n : ℕ}, (Polynomial.X ^ n - 1).Separable ↔ ↑n ≠ 0
This theorem states that for any field `F` and any natural number `n`, the polynomial `X^n - 1` is separable if and only if `n` is not equal to zero. Here, "separable" refers to a property of a polynomial that its roots are distinct. Thus, the polynomial `X^n - 1` has distinct roots (is separable) exactly when `n` is non-zero. The ↑n notation is used to coerce or convert `n` from a natural number to an element of the field `F`.
More concisely: For any field `F`, the polynomial `X^n - 1` is separable if and only if `n` is non-zero.
|
AlgEquiv.isSeparable
theorem AlgEquiv.isSeparable :
∀ {F : Type u_1} {K : Type u_2} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] {E : Type u_3}
[inst_3 : Ring E] [inst_4 : Algebra F E], (K ≃ₐ[F] E) → ∀ [inst_5 : IsSeparable F K], IsSeparable F E
This theorem states that the property of being separable, denoted as `IsSeparable`, is preserved when transferred across an algebraic equivalence (`AlgEquiv`). Specifically, given two types `K` and `E` with the structure of rings (`Ring K` and `Ring E`) and an algebra over a common ring `F` (`Algebra F K` and `Algebra F E`), if `K` is algebraically equivalent to `E` (denoted as `K ≃ₐ[F] E`), and `K` is separable over `F` (`IsSeparable F K`), then `E` is also separable over `F`. The separability of a field extension in algebra is a condition related to the roots of polynomials.
More concisely: If `K` is a separable `Ring` extension of `F` and `K` is algebraically equivalent to `E` as `Ring` extensions of `F`, then `E` is a separable extension of `F`.
|
IsSeparable.isIntegral
theorem IsSeparable.isIntegral :
∀ (F : Type u_1) {K : Type u_2} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K]
[inst_3 : IsSeparable F K] (x : K), IsIntegral F x
This theorem states that for every element `x` of a ring `K`, which is an algebra over a commutative ring `F`, the element `x` is integral if the algebra `K` over `F` is separable. In other words, the element `x` is a root of some monic polynomial with coefficients in `F`. This holds true for all types `F` and `K` where `F` is a commutative ring, `K` is a ring, `K` is an algebra over `F`, and `K` is separable over `F`.
More concisely: If `K` is a separable algebra over the commutative ring `F`, then every element `x` in `K`, being an algebra over `F`, is a root of some monic polynomial with coefficients in `F`.
|
Polynomial.Separable.of_mul_left
theorem Polynomial.Separable.of_mul_left :
∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, (f * g).Separable → f.Separable
This theorem states that for any commutative semiring `R` and for any two polynomials `f` and `g` with coefficients in `R`, if the product of `f` and `g` is a separable polynomial, then `f` itself is also a separable polynomial.
In mathematical terms, a separable polynomial is one that is coprime with its derivative. That is, a polynomial is separable if there is no non-unit common divisor for the polynomial and its derivative.
More concisely: If `R` is a commutative semiring and `f` and `g` are polynomials over `R` with separable product `fg`, then each of the polynomials `f` and `g` is separable.
|
Polynomial.separable_map
theorem Polynomial.separable_map :
∀ {F : Type u} [inst : Field F] {S : Type u_1} [inst_1 : CommRing S] [inst_2 : Nontrivial S] (f : F →+* S)
{p : Polynomial F}, (Polynomial.map f p).Separable ↔ p.Separable
This theorem states that for any field `F`, commutative ring `S`, and a ring homomorphism `f` from `F` to `S`, if a polynomial `p` over `F` is separable (meaning that it is coprime with its derivative), then the polynomial obtained by mapping `p` across the ring homomorphism `f` is also separable, and vice versa. In other words, the separability of a polynomial is preserved under the mapping operation.
More concisely: If `f` is a ring homomorphism from field `F` to commutative ring `S`, and polynomial `p` over `F` is separable, then the image of `p` under `f` is also separable. Conversely, if `p` is the image of a separable polynomial under `f`, then `p` itself is separable.
|
Polynomial.separable_def
theorem Polynomial.separable_def :
∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R), f.Separable ↔ IsCoprime f (Polynomial.derivative f) := by
sorry
The theorem `Polynomial.separable_def` states that for any commutative semiring `R` and any polynomial `f` of `R`, `f` is separable if and only if `f` and its derivative are coprime. In the context of this theorem, being coprime is defined as the existence of two elements `a` and `b` such that `a * f + b * derivative of f = 1`. This theorem therefore provides a characterization of separable polynomials in terms of their relationship with their derivatives.
More concisely: A polynomial over a commutative semiring is separable if and only if it and its derivative are coprime.
|
Polynomial.separable_X_pow_sub_C_unit
theorem Polynomial.separable_X_pow_sub_C_unit :
∀ {R : Type u} [inst : CommRing R] {n : ℕ} (u : Rˣ), IsUnit ↑n → (Polynomial.X ^ n - Polynomial.C ↑u).Separable
This theorem states that if `n` is a unit in a commutative ring `R`, then the polynomial `X^n - u` is separable for any unit `u`. In other words, if `n` has a two-sided inverse in the ring, then the polynomial defined by the difference of `X` raised to the power `n` and the constant polynomial `u` has no repeated roots. Here, `X` represents the polynomial variable, and `Polynomial.C` is used to denote the constant polynomial.
More concisely: If `n` is a unit in a commutative ring `R`, then the polynomial `X^n - u` is separable for any constant `u` in `R`.
|
Polynomial.separable_X_pow_sub_C
theorem Polynomial.separable_X_pow_sub_C :
∀ {F : Type u} [inst : Field F] {n : ℕ} (a : F), ↑n ≠ 0 → a ≠ 0 → (Polynomial.X ^ n - Polynomial.C a).Separable
The theorem `Polynomial.separable_X_pow_sub_C` states that for any field `F` and natural number `n`, if `n` is not equal to zero in `F` and `a` is a non-zero element of `F`, then the polynomial `X^n - a` is separable. Here, `X` represents the polynomial variable and `Polynomial.C a` represents the constant polynomial `a`. In mathematical terms, if $n \neq 0$ in a field $F$ and $a \neq 0$ in $F$, the polynomial $X^n - a$ is separable. This means that the polynomial has no multiple roots.
More concisely: For any field `F` and natural number `n` in `F` with `n` not equal to zero, the polynomial `X^n - Polynomial.C a` over `F` is separable when `a` is a non-zero element of `F`.
|
IsSeparable.separable
theorem IsSeparable.separable :
∀ (F : Type u_1) {K : Type u_2} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K]
[inst_3 : IsSeparable F K] (x : K), (minpoly F x).Separable
This theorem states that for any types `F` and `K`, where `F` is a commutative ring, `K` is a ring, and `F` is an algebra over `K`, if `K` is separable over `F`, then the minimal polynomial of any element `x` of `K` over `F` is a separable polynomial. Here, a polynomial being separable means that it is coprime with its derivative. The minimal polynomial of `x` over `F` is the unique monic polynomial with coefficients in `F` that has `x` as a root and has the lowest degree among all such polynomials.
More concisely: If `F` is a commutative ring, `K` is a separable extension of `F` as a ring, and `F` is an algebra over `K`, then the minimal polynomial of any element in `K` over `F` is a separable polynomial.
|
Polynomial.nodup_roots
theorem Polynomial.nodup_roots :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, p.Separable → p.roots.Nodup
This theorem states that for any polynomial `p` over a commutative ring `R` that is an integral domain, if `p` is a separable polynomial (which means it is coprime with its derivative), then the roots of `p` occur with multiplicity at most 1, i.e., there are no duplicate roots. In other words, all the roots of `p` are distinct.
More concisely: If `p` is a separable polynomial over an integral domain `R`, then `p` has no repeated roots.
|