# 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` factors in `L`.

source
def Polynomial.Splits {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (f : Polynomial K) :
Prop

A polynomial `Splits` iff it `Factors` after mapping under a ring homomorphism. This will eventually be replaced by `Polynomial.Factors`.

Equations

- Polynomial.Splits i f = (Polynomial.map i f).Factors

Instances For

source
@[simp]
theorem Polynomial.splits_zero {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) :
Splits i 0
source
theorem Polynomial.splits_of_map_eq_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} {a : L} (h : map i f = C a) :
Splits i f
source
@[simp]
theorem Polynomial.splits_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (a : K) :
Splits i (C a)
source
theorem Polynomial.splits_of_map_degree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : (map i f).degree = 1) :
Splits i f
source
theorem Polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : f.degree ≤ 1) :
Splits i f
source
theorem Polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : f.degree = 1) :
Splits i f
source
theorem Polynomial.splits_of_natDegree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : f.natDegree ≤ 1) :
Splits i f
source
theorem Polynomial.splits_of_natDegree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : f.natDegree = 1) :
Splits i f
source
theorem Polynomial.splits_mul {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f g : Polynomial K} (hf : Splits i f) (hg : Splits i g) :
Splits i (f * g)
source
theorem Polynomial.splits_of_splits_mul' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f g : Polynomial K} (hfg : map i (f * g) ≠ 0) (h : Splits i (f * g)) :
Splits i f ∧ Splits i g
source
theorem Polynomial.splits_map_iff {F : Type u} {K : Type v} [CommRing K] [Field F] {L : Type u_2} [CommRing L] (i : K →+* L) (j : L →+* F) {f : Polynomial K} :
Splits j (map i f) ↔ Splits (j.comp i) f
source
theorem Polynomial.splits_one {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) :
Splits i 1
source
theorem Polynomial.splits_of_isUnit {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) [IsDomain K] {u : Polynomial K} (hu : IsUnit u) :
Splits i u
source
theorem Polynomial.splits_X_sub_C {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {x : K} :
Splits i (X - C x)
source
theorem Polynomial.splits_X {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) :
Splits i X
source
theorem Polynomial.splits_prod {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {ι : Type u} {s : ι → Polynomial K} {t : Finset ι} :
(∀ j ∈ t, Splits i (s j)) → Splits i (∏ x ∈ t, s x)
source
theorem Polynomial.splits_pow {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Splits i f) (n : ℕ) :
Splits i (f ^ n)
source
theorem Polynomial.splits_X_pow {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) (n : ℕ) :
Splits i (X ^ n)
source
theorem Polynomial.splits_id_iff_splits {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} :
Splits (RingHom.id L) (map i f) ↔ Splits i f
source
theorem Polynomial.Splits.comp_of_map_degree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f p : Polynomial K} (hd : (map i p).degree ≤ 1) (h : Splits i f) :
Splits i (f.comp p)
source
theorem Polynomial.splits_iff_comp_splits_of_degree_eq_one {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f p : Polynomial K} (hd : (map i p).degree = 1) :
Splits i f ↔ Splits i (f.comp p)
source
theorem Polynomial.Splits.comp_of_degree_le_one {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f p : Polynomial K} (hd : p.degree ≤ 1) (h : Splits i f) :
Splits i (f.comp p)

This is a weaker variant of `Splits.comp_of_map_degree_le_one`, but its conditions are easier to check.

source
theorem Polynomial.Splits.comp_X_sub_C {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} (a : K) {f : Polynomial K} (h : Splits i f) :
Splits i (f.comp (X - C a))
source
theorem Polynomial.Splits.comp_X_add_C {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} (a : K) {f : Polynomial K} (h : Splits i f) :
Splits i (f.comp (X + C a))
source
theorem Polynomial.Splits.comp_neg_X {K : Type v} {L : Type w} [CommRing K] [Field L] {i : K →+* L} {f : Polynomial K} (h : Splits i f) :
Splits i (f.comp (-X))
source
theorem Polynomial.exists_root_of_splits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Splits i f) (hf0 : (map i f).degree ≠ 0) :
∃ (x : L), eval₂ i x f = 0
source
theorem Polynomial.roots_ne_zero_of_splits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hs : Splits i f) (hf0 : (map i f).natDegree ≠ 0) :
(map i f).roots ≠ 0
source
def Polynomial.rootOfSplits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Splits i f) (hfd : (map i f).degree ≠ 0) :
L

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

Equations

- Polynomial.rootOfSplits' i hf hfd = Classical.choose ⋯

Instances For

source
theorem Polynomial.map_rootOfSplits' {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Splits i f) (hfd : (map i f).degree ≠ 0) :
eval₂ i (rootOfSplits' i hf hfd) f = 0
source
theorem Polynomial.natDegree_eq_card_roots' {K : Type v} {L : Type w} [CommRing K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Splits i p) :
(map i p).natDegree = (map i p).roots.card
source
theorem Polynomial.degree_eq_card_roots' {K : Type v} {L : Type w} [CommRing K] [Field L] {p : Polynomial K} {i : K →+* L} (p_ne_zero : map i p ≠ 0) (hsplit : Splits i p) :
(map i p).degree = ↑(map i p).roots.card
source
theorem Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C {R : Type u_1} {L : Type w} [CommSemiring R] [CommRing L] [Algebra R L] (s : Multiset L) {x : L} (hx : x ∈ s) {p : Polynomial R} (hp : (mapAlg R L) p = (Multiset.map (fun (a : L) => X - C a) s).prod) :
(aeval x) p = 0
source
theorem Polynomial.splits_iff {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) (f : Polynomial K) :
Splits i f ↔ f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ 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 : Splits i f) :
f = 0 ∨ ∀ {g : Polynomial L}, Irreducible g → g ∣ 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 : Splits i (f * g)) :
Splits i f ∧ 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 : Splits i f) (hgf : g ∣ f) :
Splits i g
source
theorem Polynomial.splits_of_splits_gcd_left {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) [DecidableEq K] {f g : Polynomial K} (hf0 : f ≠ 0) (hf : Splits i f) :
Splits i (EuclideanDomain.gcd f g)
source
theorem Polynomial.splits_of_splits_gcd_right {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) [DecidableEq K] {f g : Polynomial K} (hg0 : g ≠ 0) (hg : Splits i g) :
Splits i (EuclideanDomain.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) :
Splits i (f * g) ↔ Splits i f ∧ 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 ∈ t, s j ≠ 0) → (Splits i (∏ x ∈ t, s x) ↔ ∀ j ∈ t, 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 : Splits (RingHom.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 : Splits i f) (hf0 : f.degree ≠ 0) :
∃ (x : L), 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 : Splits i f) (hf0 : f.natDegree ≠ 0) :
(map i f).roots ≠ 0
source
def Polynomial.rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : 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

- Polynomial.rootOfSplits i hf hfd = Polynomial.rootOfSplits' i hf ⋯

Instances For

source
theorem Polynomial.rootOfSplits'_eq_rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Splits i f) (hfd : (map i f).degree ≠ 0) :
rootOfSplits' i hf hfd = rootOfSplits i hf ⋯

`rootOfSplits'` is definitionally equal to `rootOfSplits`.

source
theorem Polynomial.map_rootOfSplits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Splits i f) (hfd : f.degree ≠ 0) :
eval₂ i (rootOfSplits i hf hfd) f = 0
source
theorem Polynomial.natDegree_eq_card_roots {K : Type v} {L : Type w} [Field K] [Field L] {p : Polynomial K} {i : K →+* L} (hsplit : Splits i p) :
p.natDegree = (map i p).roots.card
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 : Splits i p) :
p.degree = ↑(map i p).roots.card
source
theorem Polynomial.roots_map {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (hf : Splits (RingHom.id K) f) :
(map i f).roots = Multiset.map (⇑i) f.roots
source
theorem Polynomial.Splits.mem_subfield_of_isRoot {K : Type v} [Field K] (F : Subfield K) {f : Polynomial ↥F} (hnz : f ≠ 0) (hf : Splits (RingHom.id ↥F) f) {x : K} (hx : (map F.subtype f).IsRoot x) :
x ∈ F
source
theorem Polynomial.image_rootSet {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {p : Polynomial R} (h : Splits (algebraMap R K) p) (f : K →ₐ[R] L) :
⇑f '' p.rootSet K = p.rootSet L
source
theorem Polynomial.adjoin_rootSet_eq_range {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {p : Polynomial R} (h : Splits (algebraMap R K) p) (f : K →ₐ[R] L) :
Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet 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 : Splits i p) :
map i p = C (i p.leadingCoeff) * (Multiset.map (fun (a : L) => X - C a) (map i p).roots).prod
source
theorem Polynomial.eq_prod_roots_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (hsplit : Splits (RingHom.id K) p) :
p = C p.leadingCoeff * (Multiset.map (fun (a : K) => X - C a) p.roots).prod
source
theorem Polynomial.Splits.dvd_of_roots_le_roots {K : Type v} [Field K] {p q : Polynomial K} (hp : Splits (RingHom.id K) p) (hp0 : p ≠ 0) (hq : p.roots ≤ q.roots) :
p ∣ q
source
theorem Polynomial.Splits.dvd_iff_roots_le_roots {K : Type v} [Field K] {p q : Polynomial K} (hp : Splits (RingHom.id K) p) (hp0 : p ≠ 0) (hq0 : q ≠ 0) :
p ∣ q ↔ p.roots ≤ q.roots
source
theorem Polynomial.aeval_eq_prod_aroots_sub_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} (hsplit : Splits (algebraMap K L) p) (v : L) :
(aeval v) p = (algebraMap K L) p.leadingCoeff * (Multiset.map (fun (a : L) => v - a) (p.aroots L)).prod
source
theorem Polynomial.eval_eq_prod_roots_sub_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (hsplit : Splits (RingHom.id K) p) (v : K) :
eval v p = p.leadingCoeff * (Multiset.map (fun (a : K) => v - 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 : Splits (RingHom.id K) p) :
p = (Multiset.map (fun (a : K) => X - C a) p.roots).prod
source
theorem Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] {p : Polynomial K} (m : p.Monic) (hsplit : Splits (algebraMap K L) p) (v : L) :
(aeval v) p = (Multiset.map (fun (a : L) => v - a) (p.aroots L)).prod
source
theorem Polynomial.eval_eq_prod_roots_sub_of_monic_of_splits_id {K : Type v} [Field K] {p : Polynomial K} (m : p.Monic) (hsplit : Splits (RingHom.id K) p) (v : K) :
eval v p = (Multiset.map (fun (a : K) => v - 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 : Splits i h) (h_roots : (map i h).roots = {i x}) :
h = C h.leadingCoeff * (X - C x)
source
theorem Polynomial.mem_lift_of_splits_of_roots_mem_range (R : Type u_1) {K : Type v} [CommRing R] [Field K] [Algebra R K] {f : Polynomial K} (hs : Splits (RingHom.id K) f) (hm : f.Monic) (hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range) :
f ∈ lifts (algebraMap R K)
source
theorem Polynomial.splits_of_natDegree_eq_two {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {x : L} (h₁ : f.natDegree = 2) (h₂ : eval₂ i x f = 0) :
Splits i f

A polynomial of degree `2` with a root splits.

source
theorem Polynomial.splits_of_degree_eq_two {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} {x : L} (h₁ : f.degree = 2) (h₂ : eval₂ i x f = 0) :
Splits i f
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 : map i f = C (i f.leadingCoeff) * (Multiset.map (fun (a : L) => X - C a) s).prod) :
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} (h : Splits (RingHom.id K) f) :
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} :
Splits i f ↔ ∃ (s : Multiset L), map i f = C (i f.leadingCoeff) * (Multiset.map (fun (a : L) => X - C a) s).prod
source
theorem Polynomial.splits_of_comp {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 : Splits (j.comp i) f) (roots_mem_range : ∀ a ∈ (map (j.comp i) f).roots, a ∈ j.range) :
Splits i f
source
theorem Polynomial.splits_id_of_splits {K : Type v} {L : Type w} [Field K] [Field L] (i : K →+* L) {f : Polynomial K} (h : Splits i f) (roots_mem_range : ∀ a ∈ (map i f).roots, a ∈ i.range) :
Splits (RingHom.id K) f
source
theorem Polynomial.splits_comp_of_splits {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] (i : R →+* K) (j : K →+* L) {f : Polynomial R} (h : Splits i f) :
Splits (j.comp i) f
source
theorem Polynomial.splits_of_algHom {R : Type u_1} {K : Type v} {L : Type w} [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {f : Polynomial R} (h : Splits (algebraMap R K) f) (e : K →ₐ[R] L) :
Splits (algebraMap R L) f
source
theorem Polynomial.splits_of_isScalarTower {R : Type u_1} {K : Type v} (L : Type w) [CommRing R] [Field K] [Field L] [Algebra R K] [Algebra R L] {f : Polynomial R} [Algebra K L] [IsScalarTower R K L] (h : Splits (algebraMap R K) f) :
Splits (algebraMap R L) f
source
theorem Polynomial.splits_iff_card_roots {K : Type v} [Field K] {p : Polynomial K} :
Splits (RingHom.id K) p ↔ p.roots.card = p.natDegree

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

source
theorem Polynomial.eval₂_derivative_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [DecidableEq L] {P : Polynomial K} {f : K →+* L} (hP : Splits f P) (x : L) :
eval₂ f x (derivative P) = f P.leadingCoeff * (Multiset.map (fun (a : L) => (Multiset.map (fun (x_1 : L) => x - x_1) ((map f P).roots.erase a)).prod) (map f P).roots).sum
source
theorem Polynomial.aeval_derivative_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] [DecidableEq L] {P : Polynomial K} (hP : Splits (algebraMap K L) P) (r : L) :
(aeval r) (derivative P) = (algebraMap K L) P.leadingCoeff * (Multiset.map (fun (a : L) => (Multiset.map (fun (x : L) => r - x) ((P.aroots L).erase a)).prod) (P.aroots L)).sum
source
theorem Polynomial.eval_derivative_of_splits {K : Type v} [Field K] [DecidableEq K] {P : Polynomial K} (hP : Splits (RingHom.id K) P) (r : K) :
eval r (derivative P) = P.leadingCoeff * (Multiset.map (fun (a : K) => (Multiset.map (fun (x : K) => r - x) (P.roots.erase a)).prod) P.roots).sum
source
theorem Polynomial.aeval_root_derivative_of_splits {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L] [DecidableEq L] {P : Polynomial K} (hmo : P.Monic) (hP : Splits (algebraMap K L) P) {r : L} (hr : r ∈ P.aroots L) :
(aeval r) (derivative P) = (Multiset.map (fun (a : L) => r - a) ((P.aroots L).erase r)).prod

Let `P` be a monic polynomial over `K` that splits over `L`. Let `r : L` be a root of `P`. Then $P'(r) = \prod_{a}(r-a)$, where the product in the RHS is taken over all roots of `P` in `L`, with the multiplicity of `r` reduced by one.

source
theorem Polynomial.eval_derivative_eq_eval_mul_sum_of_splits {K : Type v} [Field K] {p : Polynomial K} {x : K} (h : Splits (RingHom.id K) p) (hx : eval x p ≠ 0) :
eval x (derivative p) = eval x p * (Multiset.map (fun (z : K) => 1 / (x - z)) p.roots).sum
source
theorem Polynomial.eval_derivative_div_eval_of_ne_zero_of_splits {K : Type v} [Field K] {p : Polynomial K} {x : K} (h : Splits (RingHom.id K) p) (hx : eval x p ≠ 0) :
eval x (derivative p) / eval x p = (Multiset.map (fun (z : K) => 1 / (x - z)) p.roots).sum
source
theorem Polynomial.coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits {K : Type v} [Field K] {P : Polynomial K} (hP : Splits (RingHom.id K) P) :
P.coeff 0 = (-1) ^ P.natDegree * P.leadingCoeff * P.roots.prod
source
theorem Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits {K : Type v} [Field K] {P : Polynomial K} (hmo : P.Monic) (hP : Splits (RingHom.id K) P) :
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.

source
theorem Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits {K : Type v} [Field K] {P : Polynomial K} (hP : Splits (RingHom.id K) P) :
P.nextCoeff = -P.leadingCoeff * P.roots.sum
source
theorem Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits {K : Type v} [Field K] {P : Polynomial K} (hmo : P.Monic) (hP : Splits (RingHom.id K) P) :
P.nextCoeff = -P.roots.sum

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

source
@[deprecated Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits (since := "2025-10-08")]
theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits {K : Type v} [Field K] {P : Polynomial K} (hmo : P.Monic) (hP : Splits (RingHom.id K) P) :
P.coeff 0 = (-1) ^ P.natDegree * P.roots.prod

Alias of `Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits`.

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

source
@[deprecated Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits (since := "2025-10-08")]
theorem Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split {K : Type v} [Field K] {P : Polynomial K} (hmo : P.Monic) (hP : Splits (RingHom.id K) P) :
P.nextCoeff = -P.roots.sum

Alias of `Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits`.

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