# Separable polynomials #

We define a polynomial to be separable if it is coprime with its derivative. We prove basic properties about separable polynomials here.

## Main definitions #

• Polynomial.Separable f: a polynomial f is separable iff it is coprime with its derivative.
def Polynomial.Separable {R : Type u} [] (f : ) :

A polynomial is separable iff it is coprime with its derivative.

Equations
Instances For
theorem Polynomial.separable_def {R : Type u} [] (f : ) :
IsCoprime f (Polynomial.derivative f)
theorem Polynomial.separable_def' {R : Type u} [] (f : ) :
∃ (a : ) (b : ), a * f + b * Polynomial.derivative f = 1
theorem Polynomial.Separable.ne_zero {R : Type u} [] [] {f : } (h : ) :
f 0
@[simp]
theorem Polynomial.separable_one {R : Type u} [] :
theorem Polynomial.separable_of_subsingleton {R : Type u} [] [] (f : ) :
theorem Polynomial.separable_X_add_C {R : Type u} [] (a : R) :
Polynomial.Separable (Polynomial.X + Polynomial.C a)
theorem Polynomial.separable_X {R : Type u} [] :
theorem Polynomial.separable_C {R : Type u} [] (r : R) :
Polynomial.Separable (Polynomial.C r)
theorem Polynomial.Separable.of_mul_left {R : Type u} [] {f : } {g : } (h : Polynomial.Separable (f * g)) :
theorem Polynomial.Separable.of_mul_right {R : Type u} [] {f : } {g : } (h : Polynomial.Separable (f * g)) :
theorem Polynomial.Separable.of_dvd {R : Type u} [] {f : } {g : } (hf : ) (hfg : g f) :
theorem Polynomial.separable_gcd_left {F : Type u_1} [] {f : } (hf : ) (g : ) :
theorem Polynomial.separable_gcd_right {F : Type u_1} [] {g : } (f : ) (hg : ) :
theorem Polynomial.Separable.isCoprime {R : Type u} [] {f : } {g : } (h : Polynomial.Separable (f * g)) :
theorem Polynomial.Separable.of_pow' {R : Type u} [] {f : } {n : } (_h : Polynomial.Separable (f ^ n)) :
n = 1 n = 0
theorem Polynomial.Separable.of_pow {R : Type u} [] {f : } (hf : ¬) {n : } (hn : n 0) (hfs : Polynomial.Separable (f ^ n)) :
n = 1
theorem Polynomial.Separable.map {R : Type u} [] {S : Type v} [] {p : } (h : ) {f : R →+* S} :
theorem Associated.separable {R : Type u} [] {f : } {g : } (ha : ) (h : ) :
theorem Associated.separable_iff {R : Type u} [] {f : } {g : } (ha : ) :
theorem Polynomial.Separable.mul_unit {R : Type u} [] {f : } {g : } (hf : ) (hg : ) :
theorem Polynomial.Separable.unit_mul {R : Type u} [] {f : } {g : } (hf : ) (hg : ) :
theorem Polynomial.Separable.eval₂_derivative_ne_zero {R : Type u} [] {S : Type v} [] [] (f : R →+* S) {p : } (h : ) {x : S} (hx : = 0) :
Polynomial.eval₂ f x (Polynomial.derivative p) 0
theorem Polynomial.Separable.aeval_derivative_ne_zero {R : Type u} [] {S : Type v} [] [] [Algebra R S] {p : } (h : ) {x : S} (hx : () p = 0) :
() (Polynomial.derivative p) 0
theorem Polynomial.isUnit_of_self_mul_dvd_separable {R : Type u} [] {p : } {q : } (hp : ) (hq : q * q p) :
theorem Polynomial.multiplicity_le_one_of_separable {R : Type u} [] {p : } {q : } (hq : ¬) (hsep : ) :
1
theorem Polynomial.Separable.squarefree {R : Type u} [] {p : } (hsep : ) :

A separable polynomial is square-free.

See PerfectField.separable_iff_squarefree for the converse when the coefficients are a perfect field.

theorem Polynomial.separable_X_sub_C {R : Type u} [] {x : R} :
Polynomial.Separable (Polynomial.X - Polynomial.C x)
theorem Polynomial.Separable.mul {R : Type u} [] {f : } {g : } (hf : ) (hg : ) (h : ) :
theorem Polynomial.separable_prod' {R : Type u} [] {ι : Type u_1} {f : ι} {s : } :
(xs, ys, x yIsCoprime (f x) (f y))(xs, Polynomial.Separable (f x))Polynomial.Separable (Finset.prod s fun (x : ι) => f x)
theorem Polynomial.separable_prod {R : Type u} [] {ι : Type u_1} [] {f : ι} (h1 : Pairwise (IsCoprime on f)) (h2 : ∀ (x : ι), Polynomial.Separable (f x)) :
Polynomial.Separable (Finset.prod Finset.univ fun (x : ι) => f x)
theorem Polynomial.Separable.inj_of_prod_X_sub_C {R : Type u} [] [] {ι : Type u_1} {f : ιR} {s : } (hfs : Polynomial.Separable (Finset.prod s fun (i : ι) => Polynomial.X - Polynomial.C (f i))) {x : ι} {y : ι} (hx : x s) (hy : y s) (hfxy : f x = f y) :
x = y
theorem Polynomial.Separable.injective_of_prod_X_sub_C {R : Type u} [] [] {ι : Type u_1} [] {f : ιR} (hfs : Polynomial.Separable (Finset.prod Finset.univ fun (i : ι) => Polynomial.X - Polynomial.C (f i))) :
theorem Polynomial.nodup_of_separable_prod {R : Type u} [] [] {s : } (hs : Polynomial.Separable (Multiset.prod (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s))) :
theorem Polynomial.separable_X_pow_sub_C_unit {R : Type u} [] {n : } (u : Rˣ) (hn : IsUnit n) :
Polynomial.Separable (Polynomial.X ^ n - Polynomial.C u)

If IsUnit n in a CommRing R, then X ^ n - u is separable for any unit u.

theorem Polynomial.rootMultiplicity_le_one_of_separable {R : Type u} [] [] {p : } (hsep : ) (x : R) :
theorem Polynomial.count_roots_le_one {R : Type u} [] [] {p : } (hsep : ) (x : R) :
1
theorem Polynomial.nodup_roots {R : Type u} [] [] {p : } (hsep : ) :
theorem Polynomial.separable_iff_derivative_ne_zero {F : Type u} [] {f : } (hf : ) :
Polynomial.derivative f 0
theorem Polynomial.separable_map {F : Type u} [] {S : Type u_1} [] [] (f : F →+* S) {p : } :
theorem Polynomial.separable_prod_X_sub_C_iff' {F : Type u} [] {ι : Type u_1} {f : ιF} {s : } :
Polynomial.Separable (Finset.prod s fun (i : ι) => Polynomial.X - Polynomial.C (f i)) xs, ys, f x = f yx = y
theorem Polynomial.separable_prod_X_sub_C_iff {F : Type u} [] {ι : Type u_1} [] {f : ιF} :
Polynomial.Separable (Finset.prod Finset.univ fun (i : ι) => Polynomial.X - Polynomial.C (f i))
theorem Polynomial.separable_or {F : Type u} [] (p : ) [HF : CharP F p] {f : } (hf : ) :
∃ (g : ), () g = f
theorem Polynomial.exists_separable_of_irreducible {F : Type u} [] (p : ) [HF : CharP F p] {f : } (hf : ) (hp : p 0) :
∃ (n : ) (g : ), (Polynomial.expand F (p ^ n)) g = f
theorem Polynomial.isUnit_or_eq_zero_of_separable_expand {F : Type u} [] (p : ) [HF : CharP F p] {f : } (n : ) (hp : 0 < p) (hf : Polynomial.Separable ((Polynomial.expand F (p ^ n)) f)) :
n = 0
theorem Polynomial.unique_separable_of_irreducible {F : Type u} [] (p : ) [HF : CharP F p] {f : } (hf : ) (hp : 0 < p) (n₁ : ) (g₁ : ) (hg₁ : ) (hgf₁ : (Polynomial.expand F (p ^ n₁)) g₁ = f) (n₂ : ) (g₂ : ) (hg₂ : ) (hgf₂ : (Polynomial.expand F (p ^ n₂)) g₂ = f) :
n₁ = n₂ g₁ = g₂
theorem Polynomial.separable_X_pow_sub_C {F : Type u} [] {n : } (a : F) (hn : n 0) (ha : a 0) :
Polynomial.Separable (Polynomial.X ^ n - Polynomial.C a)

If n ≠ 0 in F, then X ^ n - a is separable for any a ≠ 0.

theorem Polynomial.X_pow_sub_one_separable_iff {F : Type u} [] {n : } :
Polynomial.Separable (Polynomial.X ^ n - 1) n 0

In a field F, X ^ n - 1 is separable iff ↑n ≠ 0.

theorem Polynomial.card_rootSet_eq_natDegree {F : Type u} [] {K : Type v} [] [Algebra F K] {p : } (hsep : ) (hsplit : Polynomial.Splits () p) :
theorem Polynomial.nodup_roots_iff_of_splits {F : Type u} [] {f : } (hf : f 0) (h : ) :

If a non-zero polynomial splits, then it has no repeated roots on that field if and only if it is separable.

theorem Polynomial.nodup_aroots_iff_of_splits {F : Type u} [] {K : Type v} [] [Algebra F K] {f : } (hf : f 0) (h : Polynomial.Splits () f) :

If a non-zero polynomial over F splits in K, then it has no repeated roots on K if and only if it is separable.

theorem Polynomial.card_rootSet_eq_natDegree_iff_of_splits {F : Type u} [] {K : Type v} [] [Algebra F K] {f : } (hf : f 0) (h : Polynomial.Splits () f) :
theorem Polynomial.eq_X_sub_C_of_separable_of_root_eq {F : Type u} [] {K : Type v} [] {i : F →+* K} {x : F} {h : } (h_sep : ) (h_root : = 0) (h_splits : ) (h_roots : y, y = i x) :
h = Polynomial.C * (Polynomial.X - Polynomial.C x)
theorem Polynomial.exists_finset_of_splits {F : Type u} [] {K : Type v} [] (i : F →+* K) {f : } (sep : ) (sp : ) :
∃ (s : ), = Polynomial.C () * Finset.prod s fun (a : K) => Polynomial.X - Polynomial.C a
theorem Irreducible.separable {F : Type u} [] [] {f : } (hf : ) :
theorem isSeparable_def (F : Type u_1) (K : Type u_2) [] [Ring K] [Algebra F K] :
∀ (x : K),
class IsSeparable (F : Type u_1) (K : Type u_2) [] [Ring K] [Algebra F K] :

Typeclass for separable field extension: K is a separable field extension of F iff the minimal polynomial of every x : K is separable. This implies that K/F is an algebraic extension, because the minimal polynomial of a non-integral element is 0, which is not separable.

We define this for general (commutative) rings and only assume F and K are fields if this is needed for a proof.

• separable' : ∀ (x : K),
Instances
theorem IsSeparable.separable (F : Type u_1) {K : Type u_2} [] [Ring K] [Algebra F K] [] (x : K) :
theorem Polynomial.Separable.isIntegral {F : Type u_1} {K : Type u_2} [] [Ring K] [Algebra F K] {x : K} (h : ) :

If the minimal polynomial of x : K over F is separable, then x is integral over F, because the minimal polynomial of a non-integral element is 0, which is not separable.

theorem IsSeparable.isIntegral (F : Type u_1) {K : Type u_2} [] [Ring K] [Algebra F K] [] (x : K) :
theorem isSeparable_iff {F : Type u_1} {K : Type u_2} [] [Ring K] [Algebra F K] :
∀ (x : K),
theorem AlgEquiv.isSeparable {F : Type u_1} {K : Type u_2} [] [Ring K] [Algebra F K] {E : Type u_3} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) [] :

Transfer IsSeparable across an AlgEquiv.

theorem AlgEquiv.isSeparable_iff {F : Type u_1} {K : Type u_2} [] [Ring K] [Algebra F K] {E : Type u_3} [Ring E] [Algebra F E] (e : K ≃ₐ[F] E) :
theorem IsSeparable.isAlgebraic (F : Type u_1) (K : Type u_2) [] [Ring K] [Algebra F K] [] [] :
instance isSeparable_self (F : Type u_1) [] :
Equations
• =
instance IsSeparable.of_finite (F : Type u_1) (K : Type u_2) [] [] [Algebra F K] [] [] :

A finite field extension in characteristic 0 is separable.

Equations
• =
theorem Polynomial.Separable.map_minpoly {A : Type u_1} [] (K : Type u_2) [] [Algebra A K] {R : Type u_3} [] [Algebra A R] [Algebra K R] [] {x : R} (h : ) :

If R / K / A is an extension tower, x : R is separable over A, then it's also separable over K.

theorem isSeparable_tower_top_of_isSeparable (F : Type u_1) (K : Type u_2) (E : Type u_3) [] [] [] [Algebra F K] [Algebra F E] [Algebra K E] [] [] :
theorem isSeparable_tower_bot_of_isSeparable (F : Type u_1) (K : Type u_2) (E : Type u_3) [] [] [] [Algebra F K] [Algebra F E] [Algebra K E] [] [h : ] :
theorem IsSeparable.of_algHom (F : Type u_1) {E : Type u_3} [] [] [Algebra F E] (E' : Type u_4) [Field E'] [Algebra F E'] (f : E →ₐ[F] E') [IsSeparable F E'] :
theorem IsSeparable.of_equiv_equiv {A₁ : Type u_4} {B₁ : Type u_5} {A₂ : Type u_6} {B₂ : Type u_7} [Field A₁] [Field B₁] [Field A₂] [Field B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂) (he : RingHom.comp (algebraMap A₂ B₂) e₁ = RingHom.comp (e₂) (algebraMap A₁ B₁)) [IsSeparable A₁ B₁] :
IsSeparable A₂ B₂
theorem AlgHom.card_of_powerBasis {S : Type u_2} [] {K : Type u_4} {L : Type u_5} [] [] [Algebra K S] [Algebra K L] (pb : ) (h_sep : Polynomial.Separable (minpoly K pb.gen)) (h_splits : Polynomial.Splits () (minpoly K pb.gen)) :
Fintype.card (S →ₐ[K] L) = pb.dim