# mathlibdocumentation

field_theory.separable

# 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 #

def polynomial.separable {R : Type u} (f : polynomial R) :
Prop

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

Equations
theorem polynomial.separable_def {R : Type u} (f : polynomial R) :
theorem polynomial.separable_def' {R : Type u} (f : polynomial R) :
f.separable ∃ (a b : , a * f + = 1
theorem polynomial.not_separable_zero {R : Type u} [nontrivial R] :
theorem polynomial.separable_one {R : Type u}  :
theorem polynomial.separable_X_add_C {R : Type u} (a : R) :
theorem polynomial.separable_X {R : Type u}  :
theorem polynomial.separable_C {R : Type u} (r : R) :
theorem polynomial.separable.of_mul_left {R : Type u} {f g : polynomial R} (h : (f * g).separable) :
theorem polynomial.separable.of_mul_right {R : Type u} {f g : polynomial R} (h : (f * g).separable) :
theorem polynomial.separable.of_dvd {R : Type u} {f g : polynomial R} (hf : f.separable) (hfg : g f) :
theorem polynomial.separable_gcd_left {F : Type u_1} [field F] {f : polynomial F} (hf : f.separable) (g : polynomial F) :
theorem polynomial.separable_gcd_right {F : Type u_1} [field F] {g : polynomial F} (f : polynomial F) (hg : g.separable) :
theorem polynomial.separable.is_coprime {R : Type u} {f g : polynomial R} (h : (f * g).separable) :
g
theorem polynomial.separable.of_pow' {R : Type u} {f : polynomial R} {n : } (h : (f ^ n).separable) :
f.separable n = 1 n = 0
theorem polynomial.separable.of_pow {R : Type u} {f : polynomial R} (hf : ¬) {n : } (hn : n 0) (hfs : (f ^ n).separable) :
theorem polynomial.separable.map {R : Type u} {S : Type v} {p : polynomial R} (h : p.separable) {f : R →+* S} :
theorem polynomial.is_unit_of_self_mul_dvd_separable {R : Type u} {p q : polynomial R} (hp : p.separable) (hq : q * q p) :
theorem polynomial.multiplicity_le_one_of_separable {R : Type u} {p q : polynomial R} (hq : ¬) (hsep : p.separable) :
p 1
theorem polynomial.separable.squarefree {R : Type u} {p : polynomial R} (hsep : p.separable) :
theorem polynomial.separable_X_sub_C {R : Type u} [comm_ring R] {x : R} :
theorem polynomial.separable.mul {R : Type u} [comm_ring R] {f g : polynomial R} (hf : f.separable) (hg : g.separable) (h : g) :
(f * g).separable
theorem polynomial.separable_prod' {R : Type u} [comm_ring R] {ι : Type u_1} {f : ι → } {s : finset ι} :
(∀ (x : ι), x s∀ (y : ι), y sx yis_coprime (f x) (f y))(∀ (x : ι), x s(f x).separable)(s.prod (λ (x : ι), f x)).separable
theorem polynomial.separable_prod {R : Type u} [comm_ring R] {ι : Type u_1} [fintype ι] {f : ι → } (h1 : pairwise (is_coprime on f)) (h2 : ∀ (x : ι), (f x).separable) :
(finset.univ.prod (λ (x : ι), f x)).separable
theorem polynomial.separable.inj_of_prod_X_sub_C {R : Type u} [comm_ring R] [nontrivial R] {ι : Type u_1} {f : ι → R} {s : finset ι} (hfs : (s.prod (λ (i : ι), polynomial.X - polynomial.C (f i))).separable) {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} [comm_ring R] [nontrivial R] {ι : Type u_1} [fintype ι] {f : ι → R} (hfs : (finset.univ.prod (λ (i : ι), polynomial.X - polynomial.C (f i))).separable) :
theorem polynomial.nodup_of_separable_prod {R : Type u} [comm_ring R] [nontrivial R] {s : multiset R} (hs : (multiset.map (λ (a : R), s).prod.separable) :
theorem polynomial.separable_X_pow_sub_C_unit {R : Type u} [comm_ring R] {n : } (u : Rˣ) (hn : is_unit n) :

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

theorem polynomial.root_multiplicity_le_one_of_separable {R : Type u} [comm_ring R] [nontrivial R] {p : polynomial R} (hsep : p.separable) (x : R) :
theorem polynomial.count_roots_le_one {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hsep : p.separable) (x : R) :
1
theorem polynomial.nodup_roots {R : Type u} [comm_ring R] [is_domain R] {p : polynomial R} (hsep : p.separable) :
theorem polynomial.separable_iff_derivative_ne_zero {F : Type u} [field F] {f : polynomial F} (hf : irreducible f) :
theorem polynomial.separable_map {F : Type u} [field F] {K : Type v} [field K] (f : F →+* K) {p : polynomial F} :
theorem polynomial.separable_prod_X_sub_C_iff' {F : Type u} [field F] {ι : Type u_1} {f : ι → F} {s : finset ι} :
(s.prod (λ (i : ι), polynomial.X - polynomial.C (f i))).separable ∀ (x : ι), x s∀ (y : ι), y sf x = f yx = y
theorem polynomial.separable_prod_X_sub_C_iff {F : Type u} [field F] {ι : Type u_1} [fintype ι] {f : ι → F} :
theorem polynomial.separable_or {F : Type u} [field F] (p : ) [HF : p] {f : polynomial F} (hf : irreducible f) :
f.separable ¬f.separable ∃ (g : , p) g = f
theorem polynomial.exists_separable_of_irreducible {F : Type u} [field F] (p : ) [HF : p] {f : polynomial F} (hf : irreducible f) (hp : p 0) :
∃ (n : ) (g : , g.separable (p ^ n)) g = f
theorem polynomial.is_unit_or_eq_zero_of_separable_expand {F : Type u} [field F] (p : ) [HF : p] {f : polynomial F} (n : ) (hp : 0 < p) (hf : ( (p ^ n)) f).separable) :
n = 0
theorem polynomial.unique_separable_of_irreducible {F : Type u} [field F] (p : ) [HF : p] {f : polynomial F} (hf : irreducible f) (hp : 0 < p) (n₁ : ) (g₁ : polynomial F) (hg₁ : g₁.separable) (hgf₁ : (p ^ n₁)) g₁ = f) (n₂ : ) (g₂ : polynomial F) (hg₂ : g₂.separable) (hgf₂ : (p ^ n₂)) g₂ = f) :
n₁ = n₂ g₁ = g₂
theorem polynomial.separable_X_pow_sub_C {F : Type u} [field F] {n : } (a : F) (hn : n 0) (ha : a 0) :

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} [field F] {n : } :

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

theorem polynomial.card_root_set_eq_nat_degree {F : Type u} [field F] {K : Type v} [field K] [ K] {p : polynomial F} (hsep : p.separable) (hsplit : p) :
theorem polynomial.eq_X_sub_C_of_separable_of_root_eq {F : Type u} [field F] {K : Type v} [field K] {i : F →+* K} {x : F} {h : polynomial F} (h_sep : h.separable) (h_root : = 0) (h_splits : h) (h_roots : ∀ (y : K), y h).rootsy = i x) :
theorem polynomial.exists_finset_of_splits {F : Type u} [field F] {K : Type v} [field K] (i : F →+* K) {f : polynomial F} (sep : f.separable) (sp : f) :
∃ (s : finset K), = * s.prod (λ (a : K),
theorem irreducible.separable {F : Type u} [field F] [char_zero F] {f : polynomial F} (hf : irreducible f) :
@[class]
structure is_separable (F : Type u_1) (K : Type u_2) [comm_ring F] [ring K] [ K] :
Prop
• is_integral' : ∀ (x : K), x
• separable' : ∀ (x : K), (minpoly F x).separable

Typeclass for separable field extension: K is a separable field extension of F iff the minimal polynomial of every x : K is separable.

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

Instances of this typeclass
theorem is_separable.is_integral (F : Type u_1) {K : Type u_2} [comm_ring F] [ring K] [ K] [ K] (x : K) :
x
theorem is_separable.separable (F : Type u_1) {K : Type u_2} [comm_ring F] [ring K] [ K] [ K] (x : K) :
theorem is_separable_iff {F : Type u_1} {K : Type u_2} [comm_ring F] [ring K] [ K] :
K ∀ (x : K), x (minpoly F x).separable
@[protected, instance]
def is_separable_self (F : Type u_1) [field F] :
F
@[protected, instance]
def is_separable.of_finite (F : Type u_1) (K : Type u_2) [field F] [field K] [ K] [ K] [char_zero F] :
K

A finite field extension in characteristic 0 is separable.

theorem is_separable_tower_top_of_is_separable (F : Type u_1) (K : Type u_2) (E : Type u_3) [field F] [field K] [field E] [ K] [ E] [ E] [ E] [ E] :
E
theorem is_separable_tower_bot_of_is_separable (F : Type u_1) (K : Type u_2) (E : Type u_3) [field F] [field K] [field E] [ K] [ E] [ E] [ E] [h : E] :
K
theorem is_separable.of_alg_hom (F : Type u_1) {E : Type u_3} [field F] [field E] [ E] (E' : Type u_2) [field E'] [ E'] (f : E →ₐ[F] E') [ E'] :
E
theorem alg_hom.card_of_power_basis {S : Type u_2} [comm_ring S] {K : Type u_4} {L : Type u_5} [field K] [field L] [ S] [ L] (pb : S) (h_sep : (minpoly K pb.gen).separable) (h_splits : (minpoly K pb.gen)) :