# Documentation

Mathlib.Data.Polynomial.Splits

# Split polynomials #

A polynomial f : K[X] splits over a field extension L of K if it is zero or all of its irreducible factors over L have degree 1.

## Main definitions #

• Polynomial.Splits i f: A predicate on a homomorphism i : K →+* L from a commutative ring to a field and a polynomial f saying that f.map i is zero or all of its irreducible factors over L have degree 1.

## Main statements #

• lift_of_splits: If K and L are field extensions of a field F and for some finite subset S of K, the minimal polynomial of every x ∈ K splits as a polynomial with coefficients in L, then Algebra.adjoin F S embeds into L.
def Polynomial.Splits {K : Type v} {L : Type w} [] [] (i : K →+* L) (f : ) :

A polynomial Splits iff it is zero or all of its irreducible factors have degree 1.

Instances For
@[simp]
theorem Polynomial.splits_zero {K : Type v} {L : Type w} [] [] (i : K →+* L) :
theorem Polynomial.splits_of_map_eq_C {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {a : L} (h : = Polynomial.C a) :
@[simp]
theorem Polynomial.splits_C {K : Type v} {L : Type w} [] [] (i : K →+* L) (a : K) :
Polynomial.Splits i (Polynomial.C a)
theorem Polynomial.splits_of_map_degree_eq_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : = 1) :
theorem Polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) :
theorem Polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) :
theorem Polynomial.splits_of_natDegree_le_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) :
theorem Polynomial.splits_of_natDegree_eq_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) :
theorem Polynomial.splits_mul {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {g : } (hf : ) (hg : ) :
theorem Polynomial.splits_of_splits_mul' {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {g : } (hfg : Polynomial.map i (f * g) 0) (h : Polynomial.Splits i (f * g)) :
theorem Polynomial.splits_map_iff {F : Type u} {K : Type v} {L : Type w} [] [] [] (i : K →+* L) (j : L →+* F) {f : } :
theorem Polynomial.splits_one {K : Type v} {L : Type w} [] [] (i : K →+* L) :
theorem Polynomial.splits_of_isUnit {K : Type v} {L : Type w} [] [] (i : K →+* L) [] {u : } (hu : ) :
theorem Polynomial.splits_X_sub_C {K : Type v} {L : Type w} [] [] (i : K →+* L) {x : K} :
Polynomial.Splits i (Polynomial.X - Polynomial.C x)
theorem Polynomial.splits_X {K : Type v} {L : Type w} [] [] (i : K →+* L) :
Polynomial.Splits i Polynomial.X
theorem Polynomial.splits_prod {K : Type v} {L : Type w} [] [] (i : K →+* L) {ι : Type u} {s : ι} {t : } :
(∀ (j : ι), j tPolynomial.Splits i (s j)) → Polynomial.Splits i (Finset.prod t fun x => s x)
theorem Polynomial.splits_pow {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (n : ) :
theorem Polynomial.splits_X_pow {K : Type v} {L : Type w} [] [] (i : K →+* L) (n : ) :
Polynomial.Splits i (Polynomial.X ^ n)
theorem Polynomial.splits_id_iff_splits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } :
theorem Polynomial.exists_root_of_splits' {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hs : ) (hf0 : 0) :
x, = 0
theorem Polynomial.roots_ne_zero_of_splits' {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hs : ) (hf0 : ) :
0
def Polynomial.rootOfSplits' {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (hfd : 0) :
L

Pick a root of a polynomial that splits. See rootOfSplits for polynomials over a field which has simpler assumptions.

Instances For
theorem Polynomial.map_rootOfSplits' {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (hfd : 0) :
theorem Polynomial.natDegree_eq_card_roots' {K : Type v} {L : Type w} [] [] {p : } {i : K →+* L} (hsplit : ) :
= Multiset.card ()
theorem Polynomial.degree_eq_card_roots' {K : Type v} {L : Type w} [] [] {p : } {i : K →+* L} (p_ne_zero : 0) (hsplit : ) :
= ↑(Multiset.card ())
theorem Polynomial.splits_iff {K : Type v} {L : Type w} [] [] (i : K →+* L) (f : ) :
f = 0 ∀ {g : }, g

This lemma is for polynomials over a field.

theorem Polynomial.Splits.def {K : Type v} {L : Type w} [] [] {i : K →+* L} {f : } (h : ) :
f = 0 ∀ {g : }, g

This lemma is for polynomials over a field.

theorem Polynomial.splits_of_splits_mul {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {g : } (hfg : f * g 0) (h : Polynomial.Splits i (f * g)) :
theorem Polynomial.splits_of_splits_of_dvd {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {g : } (hf0 : f 0) (hf : ) (hgf : g f) :
theorem Polynomial.splits_of_splits_gcd_left {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {g : } (hf0 : f 0) (hf : ) :
theorem Polynomial.splits_of_splits_gcd_right {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {g : } (hg0 : g 0) (hg : ) :
theorem Polynomial.splits_mul_iff {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {g : } (hf : f 0) (hg : g 0) :
theorem Polynomial.splits_prod_iff {K : Type v} {L : Type w} [] [] (i : K →+* L) {ι : Type u} {s : ι} {t : } :
(∀ (j : ι), j ts j 0) → (Polynomial.Splits i (Finset.prod t fun x => s x) ∀ (j : ι), j tPolynomial.Splits i (s j))
theorem Polynomial.degree_eq_one_of_irreducible_of_splits {K : Type v} [] {p : } (hp : ) (hp_splits : ) :
theorem Polynomial.exists_root_of_splits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hs : ) (hf0 : ) :
x, = 0
theorem Polynomial.roots_ne_zero_of_splits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hs : ) (hf0 : ) :
0
def Polynomial.rootOfSplits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (hfd : ) :
L

Pick a root of a polynomial that splits. This version is for polynomials over a field and has simpler assumptions.

Instances For
theorem Polynomial.rootOfSplits'_eq_rootOfSplits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (hfd : 0) :

rootOfSplits' is definitionally equal to rootOfSplits.

theorem Polynomial.map_rootOfSplits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (hfd : ) :
theorem Polynomial.natDegree_eq_card_roots {K : Type v} {L : Type w} [] [] {p : } {i : K →+* L} (hsplit : ) :
= Multiset.card ()
theorem Polynomial.degree_eq_card_roots {K : Type v} {L : Type w} [] [] {p : } {i : K →+* L} (p_ne_zero : p 0) (hsplit : ) :
= ↑(Multiset.card ())
theorem Polynomial.roots_map {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) :
= Multiset.map (i) ()
theorem Polynomial.image_rootSet {F : Type u} {K : Type v} {L : Type w} [] [] [] [Algebra F K] [Algebra F L] {p : } (h : Polynomial.Splits () p) (f : K →ₐ[F] L) :
f '' =
theorem Polynomial.adjoin_rootSet_eq_range {F : Type u} {K : Type v} {L : Type w} [] [] [] [Algebra F K] [Algebra F L] {p : } (h : Polynomial.Splits () p) (f : K →ₐ[F] L) :
theorem Polynomial.eq_prod_roots_of_splits {K : Type v} {L : Type w} [] [] {p : } {i : K →+* L} (hsplit : ) :
= Polynomial.C (i ()) * Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ())
theorem Polynomial.eq_prod_roots_of_splits_id {K : Type v} [] {p : } (hsplit : ) :
p = Polynomial.C () * Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ())
theorem Polynomial.eq_prod_roots_of_monic_of_splits_id {K : Type v} [] {p : } (m : ) (hsplit : ) :
p = Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) ())
theorem Polynomial.eq_X_sub_C_of_splits_of_single_root {K : Type v} {L : Type w} [] [] (i : K →+* L) {x : K} {h : } (h_splits : ) (h_roots : = {i x}) :
h = Polynomial.C () * (Polynomial.X - Polynomial.C x)
theorem Polynomial.mem_lift_of_splits_of_roots_mem_range {K : Type v} [] (R : Type u_1) [] [Algebra R K] {f : } (hs : ) (hm : ) (hr : ∀ (a : K), a RingHom.range ()) :
f
theorem Polynomial.splits_of_exists_multiset {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {s : } (hs : = Polynomial.C (i ()) * Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s)) :
theorem Polynomial.splits_of_splits_id {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } :
theorem Polynomial.splits_iff_exists_multiset {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } :
s, = Polynomial.C (i ()) * Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s)
theorem Polynomial.splits_comp_of_splits {F : Type u} {K : Type v} {L : Type w} [] [] [] (i : K →+* L) (j : L →+* F) {f : } (h : ) :
theorem Polynomial.splits_iff_card_roots {K : Type v} [] {p : } :
Multiset.card () =

A polynomial splits if and only if it has as many roots as its degree.

theorem Polynomial.aeval_root_derivative_of_splits {K : Type v} {L : Type w} [] [] [Algebra K L] {P : } (hmo : ) (hP : Polynomial.Splits () P) {r : L} (hr : r ) :
↑() (Polynomial.derivative P) = Multiset.prod (Multiset.map (fun a => r - a) ())
theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split {K : Type v} [] {P : } (hmo : ) (hP : ) :
=

If P is a monic polynomial that splits, then coeff P 0 equals the product of the roots.

theorem Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split {K : Type v} [] {P : } (hmo : ) (hP : ) :

If P is a monic polynomial that splits, then P.nextCoeff equals the sum of the roots.