mathlib3 documentation

data.polynomial.splits

Split polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Main statements #

source
def polynomial.splits {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) (f : polynomial K) :
Prop

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

Equations
source
@[simp]
theorem polynomial.splits_zero {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) :
polynomial.splits i 0
source
theorem polynomial.splits_of_map_eq_C {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} {a : L} (h : polynomial.map i f = ⇑polynomial.C a) :
polynomial.splits i f
source
@[simp]
theorem polynomial.splits_C {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) (a : K) :
polynomial.splits i (⇑polynomial.C a)
source
theorem polynomial.splits_of_map_degree_eq_one {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hf : (polynomial.map i f).degree = 1) :
polynomial.splits i f
source
theorem polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.degree ≤ 1) :
polynomial.splits i f
source
theorem polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.degree = 1) :
polynomial.splits i f
source
theorem polynomial.splits_of_nat_degree_le_one {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.nat_degree ≤ 1) :
polynomial.splits i f
source
theorem polynomial.splits_of_nat_degree_eq_one {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.nat_degree = 1) :
polynomial.splits i f
source
theorem polynomial.splits_mul {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f g : polynomial K} (hf : polynomial.splits i f) (hg : polynomial.splits i g) :
polynomial.splits i (f * g)
source
theorem polynomial.splits_of_splits_mul' {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f g : polynomial K} (hfg : polynomial.map i (f * g) ≠ 0) (h : polynomial.splits i (f * g)) :
polynomial.splits i f ∧ polynomial.splits i g
source
theorem polynomial.splits_map_iff {F : Type u} {K : Type v} {L : Type w} [comm_ring K] [field L] [field F] (i : K →+* L) (j : L →+* F) {f : polynomial K} :
polynomial.splits j (polynomial.map i f) ↔ polynomial.splits (j.comp i) f
source
theorem polynomial.splits_one {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) :
polynomial.splits i 1
source
theorem polynomial.splits_of_is_unit {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) [is_domain K] {u : polynomial K} (hu : is_unit u) :
polynomial.splits i u
source
theorem polynomial.splits_X_sub_C {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {x : K} :
polynomial.splits i (polynomial.X - ⇑polynomial.C x)
source
theorem polynomial.splits_X {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) :
polynomial.splits i polynomial.X
source
theorem polynomial.splits_prod {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {ι : Type u} {s : ι → polynomial K} {t : finset ι} :
(∀ (j : ι), j ∈ t → polynomial.splits i (s j)) → polynomial.splits i (t.prod (λ (x : ι), s x))
source
theorem polynomial.splits_pow {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits i f) (n : ℕ) :
polynomial.splits i (f ^ n)
source
theorem polynomial.splits_X_pow {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) (n : ℕ) :
polynomial.splits i (polynomial.X ^ n)
source
theorem polynomial.splits_id_iff_splits {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} :
polynomial.splits (ring_hom.id L) (polynomial.map i f) ↔ polynomial.splits i f
source
theorem polynomial.exists_root_of_splits' {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hs : polynomial.splits i f) (hf0 : (polynomial.map i f).degree ≠ 0) :
∃ (x : L), polynomial.eval₂ i x f = 0
source
theorem polynomial.roots_ne_zero_of_splits' {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hs : polynomial.splits i f) (hf0 : (polynomial.map i f).nat_degree ≠ 0) :
(polynomial.map i f).roots ≠ 0
source
noncomputable def polynomial.root_of_splits' {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits i f) (hfd : (polynomial.map i f).degree ≠ 0) :
L

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

Equations
source
theorem polynomial.map_root_of_splits' {K : Type v} {L : Type w} [comm_ring K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits i f) (hfd : (polynomial.map i f).degree ≠ 0) :
polynomial.eval₂ i (polynomial.root_of_splits' i hf hfd) f = 0
source
theorem polynomial.nat_degree_eq_card_roots' {K : Type v} {L : Type w} [comm_ring K] [field L] {p : polynomial K} {i : K →+* L} (hsplit : polynomial.splits i p) :
(polynomial.map i p).nat_degree = ⇑multiset.card (polynomial.map i p).roots
source
theorem polynomial.degree_eq_card_roots' {K : Type v} {L : Type w} [comm_ring K] [field L] {p : polynomial K} {i : K →+* L} (p_ne_zero : polynomial.map i p ≠ 0) (hsplit : polynomial.splits i p) :
(polynomial.map i p).degree = ↑(⇑multiset.card (polynomial.map i p).roots)
source
theorem polynomial.splits_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (f : polynomial K) :
polynomial.splits i f ↔ f = 0 ∨ ∀ {g : polynomial L}, irreducible g → g ∣ polynomial.map i f → g.degree = 1

This lemma is for polynomials over a field.

source
theorem polynomial.splits.def {K : Type v} {L : Type w} [field K] [field L] {i : K →+* L} {f : polynomial K} (h : polynomial.splits i f) :
f = 0 ∨ ∀ {g : polynomial L}, irreducible g → g ∣ polynomial.map i f → g.degree = 1

This lemma is for polynomials over a field.

source
theorem polynomial.splits_of_splits_mul {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hfg : f * g ≠ 0) (h : polynomial.splits i (f * g)) :
polynomial.splits i f ∧ polynomial.splits i g
source
theorem polynomial.splits_of_splits_of_dvd {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf0 : f ≠ 0) (hf : polynomial.splits i f) (hgf : g ∣ f) :
polynomial.splits i g
source
theorem polynomial.splits_of_splits_gcd_left {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf0 : f ≠ 0) (hf : polynomial.splits i f) :
polynomial.splits i (euclidean_domain.gcd f g)
source
theorem polynomial.splits_of_splits_gcd_right {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hg0 : g ≠ 0) (hg : polynomial.splits i g) :
polynomial.splits i (euclidean_domain.gcd f g)
source
theorem polynomial.splits_mul_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf : f ≠ 0) (hg : g ≠ 0) :
polynomial.splits i (f * g) ↔ polynomial.splits i f ∧ polynomial.splits i g
source
theorem polynomial.splits_prod_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {ι : Type u} {s : ι → polynomial K} {t : finset ι} :
(∀ (j : ι), j ∈ t → s j ≠ 0) → (polynomial.splits i (t.prod (λ (x : ι), s x)) ↔ ∀ (j : ι), j ∈ t → polynomial.splits i (s j))
source
theorem polynomial.degree_eq_one_of_irreducible_of_splits {K : Type v} [field K] {p : polynomial K} (hp : irreducible p) (hp_splits : polynomial.splits (ring_hom.id K) p) :
p.degree = 1
source
theorem polynomial.exists_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hs : polynomial.splits i f) (hf0 : f.degree ≠ 0) :
∃ (x : L), polynomial.eval₂ i x f = 0
source
theorem polynomial.roots_ne_zero_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hs : polynomial.splits i f) (hf0 : f.nat_degree ≠ 0) :
(polynomial.map i f).roots ≠ 0
source
noncomputable def polynomial.root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits i f) (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
source
theorem polynomial.root_of_splits'_eq_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits i f) (hfd : (polynomial.map i f).degree ≠ 0) :
polynomial.root_of_splits' i hf hfd = polynomial.root_of_splits i hf _

root_of_splits' is definitionally equal to root_of_splits.

source
theorem polynomial.map_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits i f) (hfd : f.degree ≠ 0) :
polynomial.eval₂ i (polynomial.root_of_splits i hf hfd) f = 0
source
theorem polynomial.nat_degree_eq_card_roots {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (hsplit : polynomial.splits i p) :
p.nat_degree = ⇑multiset.card (polynomial.map i p).roots
source
theorem polynomial.degree_eq_card_roots {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (p_ne_zero : p ≠ 0) (hsplit : polynomial.splits i p) :
p.degree = ↑(⇑multiset.card (polynomial.map i p).roots)
source
theorem polynomial.roots_map {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits (ring_hom.id K) f) :
(polynomial.map i f).roots = multiset.map ⇑i f.roots
source
theorem polynomial.image_root_set {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] [algebra F K] [algebra F L] {p : polynomial F} (h : polynomial.splits (algebra_map F K) p) (f : K →ₐ[F] L) :
⇑f '' p.root_set K = p.root_set L
source
theorem polynomial.adjoin_root_set_eq_range {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] [algebra F K] [algebra F L] {p : polynomial F} (h : polynomial.splits (algebra_map F K) p) (f : K →ₐ[F] L) :
algebra.adjoin F (p.root_set L) = f.range ↔ algebra.adjoin F (p.root_set K) = ⊤
source
theorem polynomial.eq_prod_roots_of_splits {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (hsplit : polynomial.splits i p) :
polynomial.map i p = ⇑polynomial.C (⇑i p.leading_coeff) * (multiset.map (λ (a : L), polynomial.X - ⇑polynomial.C a) (polynomial.map i p).roots).prod
source
theorem polynomial.eq_prod_roots_of_splits_id {K : Type v} [field K] {p : polynomial K} (hsplit : polynomial.splits (ring_hom.id K) p) :
p = ⇑polynomial.C p.leading_coeff * (multiset.map (λ (a : K), polynomial.X - ⇑polynomial.C a) p.roots).prod
source
theorem polynomial.eq_prod_roots_of_monic_of_splits_id {K : Type v} [field K] {p : polynomial K} (m : p.monic) (hsplit : polynomial.splits (ring_hom.id K) p) :
p = (multiset.map (λ (a : K), polynomial.X - ⇑polynomial.C a) p.roots).prod
source
theorem polynomial.eq_X_sub_C_of_splits_of_single_root {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {x : K} {h : polynomial K} (h_splits : polynomial.splits i h) (h_roots : (polynomial.map i h).roots = {⇑i x}) :
h = ⇑polynomial.C h.leading_coeff * (polynomial.X - ⇑polynomial.C x)
source
theorem polynomial.mem_lift_of_splits_of_roots_mem_range {K : Type v} [field K] (R : Type u_1) [comm_ring R] [algebra R K] {f : polynomial K} (hs : polynomial.splits (ring_hom.id K) f) (hm : f.monic) (hr : ∀ (a : K), a ∈ f.roots → a ∈ (algebra_map R K).range) :
f ∈ polynomial.lifts (algebra_map R K)
source
theorem polynomial.splits_of_exists_multiset {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} {s : multiset L} (hs : polynomial.map i f = ⇑polynomial.C (⇑i f.leading_coeff) * (multiset.map (λ (a : L), polynomial.X - ⇑polynomial.C a) s).prod) :
polynomial.splits i f
source
theorem polynomial.splits_of_splits_id {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} :
polynomial.splits (ring_hom.id K) f → polynomial.splits i f
source
theorem polynomial.splits_iff_exists_multiset {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} :
polynomial.splits i f ↔ ∃ (s : multiset L), polynomial.map i f = ⇑polynomial.C (⇑i f.leading_coeff) * (multiset.map (λ (a : L), polynomial.X - ⇑polynomial.C a) s).prod
source
theorem polynomial.splits_comp_of_splits {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] (i : K →+* L) (j : L →+* F) {f : polynomial K} (h : polynomial.splits i f) :
polynomial.splits (j.comp i) f
source
theorem polynomial.splits_iff_card_roots {K : Type v} [field K] {p : polynomial K} :
polynomial.splits (ring_hom.id K) p ↔ ⇑multiset.card p.roots = p.nat_degree

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

source
theorem polynomial.aeval_root_derivative_of_splits {K : Type v} {L : Type w} [field K] [field L] [algebra K L] {P : polynomial K} (hmo : P.monic) (hP : polynomial.splits (algebra_map K L) P) {r : L} (hr : r ∈ (polynomial.map (algebra_map K L) P).roots) :
⇑(polynomial.aeval r) (⇑polynomial.derivative P) = (multiset.map (λ (a : L), r - a) ((polynomial.map (algebra_map K L) P).roots.erase r)).prod
source
theorem polynomial.prod_roots_eq_coeff_zero_of_monic_of_split {K : Type v} [field K] {P : polynomial K} (hmo : P.monic) (hP : polynomial.splits (ring_hom.id K) P) :
P.coeff 0 = (-1) ^ P.nat_degree * P.roots.prod

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

source
theorem polynomial.sum_roots_eq_next_coeff_of_monic_of_split {K : Type v} [field K] {P : polynomial K} (hmo : P.monic) (hP : polynomial.splits (ring_hom.id K) P) :
P.next_coeff = -P.roots.sum

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