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

Equations
• = ( = 0 ∀ {g : }, g g.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 : ().degree = 1) :
theorem Polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : f.degree 1) :
theorem Polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : f.degree = 1) :
theorem Polynomial.splits_of_natDegree_le_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : f.natDegree 1) :
theorem Polynomial.splits_of_natDegree_eq_one {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : f.natDegree = 1) :
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 : } :
Polynomial.Splits (j.comp i) 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 : } :
(jt, Polynomial.Splits i (s j))Polynomial.Splits i (t.prod 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 : ().degree 0) :
∃ (x : L), = 0
theorem Polynomial.roots_ne_zero_of_splits' {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hs : ) (hf0 : ().natDegree 0) :
().roots 0
def Polynomial.rootOfSplits' {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (hfd : ().degree 0) :
L

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

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

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 g.degree = 1

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 : } :
(jt, s j 0)(Polynomial.Splits i (t.prod fun (x : ι) => s x) jt, Polynomial.Splits i (s j))
theorem Polynomial.degree_eq_one_of_irreducible_of_splits {K : Type v} [] {p : } (hp : ) (hp_splits : ) :
p.degree = 1
theorem Polynomial.exists_root_of_splits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hs : ) (hf0 : f.degree 0) :
∃ (x : L), = 0
theorem Polynomial.roots_ne_zero_of_splits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hs : ) (hf0 : f.natDegree 0) :
().roots 0
def Polynomial.rootOfSplits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (hfd : f.degree 0) :
L

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

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

rootOfSplits' is definitionally equal to rootOfSplits.

theorem Polynomial.map_rootOfSplits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) (hfd : f.degree 0) :
theorem Polynomial.natDegree_eq_card_roots {K : Type v} {L : Type w} [] [] {p : } {i : K →+* L} (hsplit : ) :
p.natDegree = Multiset.card ().roots
theorem Polynomial.degree_eq_card_roots {K : Type v} {L : Type w} [] [] {p : } {i : K →+* L} (p_ne_zero : p 0) (hsplit : ) :
p.degree = (Multiset.card ().roots)
theorem Polynomial.roots_map {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (hf : ) :
().roots = Multiset.map (i) f.roots
theorem Polynomial.image_rootSet {R : Type u_1} {K : Type v} {L : Type w} [] [] [] [Algebra R K] [Algebra R L] {p : } (h : Polynomial.Splits () p) (f : K →ₐ[R] L) :
f '' p.rootSet K = p.rootSet L
theorem Polynomial.adjoin_rootSet_eq_range {R : Type u_1} {K : Type v} {L : Type w} [] [] [] [Algebra R K] [Algebra R L] {p : } (h : Polynomial.Splits () p) (f : K →ₐ[R] L) :
Algebra.adjoin R (p.rootSet L) = f.range Algebra.adjoin R (p.rootSet K) =
theorem Polynomial.eq_prod_roots_of_splits {K : Type v} {L : Type w} [] [] {p : } {i : K →+* L} (hsplit : ) :
= Polynomial.C (i p.leadingCoeff) * (Multiset.map (fun (a : L) => Polynomial.X - Polynomial.C a) ().roots).prod
theorem Polynomial.eq_prod_roots_of_splits_id {K : Type v} [] {p : } (hsplit : ) :
p = Polynomial.C p.leadingCoeff * (Multiset.map (fun (a : K) => Polynomial.X - Polynomial.C a) p.roots).prod
theorem Polynomial.eq_prod_roots_of_monic_of_splits_id {K : Type v} [] {p : } (m : p.Monic) (hsplit : ) :
p = (Multiset.map (fun (a : K) => Polynomial.X - Polynomial.C a) p.roots).prod
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 : ().roots = {i x}) :
h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)
theorem Polynomial.mem_lift_of_splits_of_roots_mem_range (R : Type u_1) {K : Type v} [] [] [Algebra R K] {f : } (hs : ) (hm : f.Monic) (hr : af.roots, a ().range) :
f
theorem Polynomial.splits_of_exists_multiset {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } {s : } (hs : = Polynomial.C (i f.leadingCoeff) * (Multiset.map (fun (a : L) => Polynomial.X - Polynomial.C a) s).prod) :
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 f.leadingCoeff) * (Multiset.map (fun (a : L) => Polynomial.X - Polynomial.C a) s).prod
theorem Polynomial.splits_of_comp {F : Type u} {K : Type v} {L : Type w} [] [] [] (i : K →+* L) (j : L →+* F) {f : } (h : Polynomial.Splits (j.comp i) f) (roots_mem_range : a(Polynomial.map (j.comp i) f).roots, a j.range) :
theorem Polynomial.splits_id_of_splits {K : Type v} {L : Type w} [] [] (i : K →+* L) {f : } (h : ) (roots_mem_range : a().roots, a i.range) :
theorem Polynomial.splits_comp_of_splits {R : Type u_1} {K : Type v} {L : Type w} [] [] [] (i : R →+* K) (j : K →+* L) {f : } (h : ) :
Polynomial.Splits (j.comp i) f
theorem Polynomial.splits_of_algHom {R : Type u_1} {K : Type v} {L : Type w} [] [] [] [Algebra R K] [Algebra R L] {f : } (h : Polynomial.Splits () f) (e : K →ₐ[R] L) :
theorem Polynomial.splits_of_isScalarTower {R : Type u_1} {K : Type v} (L : Type w) [] [] [] [Algebra R K] [Algebra R L] {f : } [Algebra K L] [] (h : Polynomial.Splits () f) :
theorem Polynomial.splits_iff_card_roots {K : Type v} [] {p : } :
Multiset.card p.roots = p.natDegree

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 : P.Monic) (hP : Polynomial.Splits () P) {r : L} (hr : r P.aroots L) :
() (Polynomial.derivative P) = (Multiset.map (fun (a : L) => r - a) ((P.aroots L).erase r)).prod
theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split {K : Type v} [] {P : } (hmo : P.Monic) (hP : ) :
P.coeff 0 = (-1) ^ P.natDegree * P.roots.prod

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 : P.Monic) (hP : ) :
P.nextCoeff = -P.roots.sum

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