Split polynomials

A polynomial f : R[X] splits if it is a product of constant and monic linear polynomials.

Main definitions

• Polynomial.Splits f: A predicate on a polynomial f saying that f is a product of constant and monic linear polynomials.

def Polynomial.Splits {R : Type u_1} [Semiring R] (f : Polynomial R) : Prop

A polynomial Splits if it is a product of constant and monic linear polynomials.

@[simp]

theorem Polynomial.Splits.C {R : Type u_1} [Semiring R] (a : R) : (C a).Splits

@[simp]

theorem Polynomial.Splits.zero {R : Type u_1} [Semiring R] : Splits 0

@[simp]

theorem Polynomial.Splits.one {R : Type u_1} [Semiring R] : Splits 1

@[simp]

theorem Polynomial.Splits.X_add_C {R : Type u_1} [Semiring R] (a : R) : (X + C a).Splits

@[simp]

theorem Polynomial.Splits.X {R : Type u_1} [Semiring R] : X.Splits

@[simp]

theorem Polynomial.Splits.mul {R : Type u_1} [Semiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.Splits) : (f * g).Splits

theorem Polynomial.Splits.C_mul {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) (a : R) : (C a * f).Splits

@[simp]

theorem Polynomial.Splits.listProd {R : Type u_1} [Semiring R] {l : List (Polynomial R)} (h : ∀ f ∈ l, f.Splits) : l.prod.Splits

@[simp]

theorem Polynomial.Splits.pow {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) (n : ℕ) : (f ^ n).Splits

theorem Polynomial.Splits.X_pow {R : Type u_1} [Semiring R] (n : ℕ) : (X ^ n).Splits

theorem Polynomial.Splits.C_mul_X_pow {R : Type u_1} [Semiring R] (a : R) (n : ℕ) : (C a * X ^ n).Splits

@[simp]

theorem Polynomial.Splits.monomial {R : Type u_1} [Semiring R] (n : ℕ) (a : R) : ((Polynomial.monomial n) a).Splits

theorem Polynomial.Splits.map {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) {S : Type u_2} [Semiring S] (i : R →+* S) : (map i f).Splits

theorem Polynomial.splits_of_natDegree_eq_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree = 0) : f.Splits

theorem Polynomial.splits_of_degree_le_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 0) : f.Splits

theorem IsUnit.splits {R : Type u_1} [Semiring R] [NoZeroDivisors R] {f : Polynomial R} (hf : IsUnit f) : f.Splits

@[deprecated IsUnit.splits (since := "2025-11-27")]

theorem Polynomial.splits_of_isUnit {R : Type u_1} [Semiring R] [NoZeroDivisors R] {f : Polynomial R} (hf : IsUnit f) : f.Splits

Alias of IsUnit.splits.

theorem Polynomial.splits_of_natDegree_le_one_of_invertible {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits

theorem Polynomial.splits_of_degree_le_one_of_invertible {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : Invertible f.leadingCoeff) : f.Splits

theorem Polynomial.splits_of_natDegree_le_one_of_monic {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) (h : f.Monic) : f.Splits

theorem Polynomial.splits_of_degree_le_one_of_monic {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 1) (h : f.Monic) : f.Splits

@[simp]

theorem Polynomial.Splits.multisetProd {R : Type u_1} [CommSemiring R] {m : Multiset (Polynomial R)} (hm : ∀ f ∈ m, f.Splits) : m.prod.Splits

@[simp]

theorem Polynomial.Splits.prod {R : Type u_1} [CommSemiring R] {ι : Type u_2} {f : ι → Polynomial R} {s : Finset ι} (h : ∀ i ∈ s, (f i).Splits) : (∏ i ∈ s, f i).Splits

theorem Polynomial.Splits.taylor {R : Type u_1} [CommSemiring R] {p : Polynomial R} (hp : p.Splits) (r : R) : ((Polynomial.taylor r) p).Splits

theorem Polynomial.splits_iff_exists_multiset' {R : Type u_1} [CommSemiring R] {f : Polynomial R} : f.Splits ↔ ∃ (m : Multiset R), f = C f.leadingCoeff * (Multiset.map (fun (x : R) => X + C x) m).prod

See splits_iff_exists_multiset for the version with subtraction.

theorem Polynomial.Splits.natDegree_le_one_of_irreducible {R : Type u_1} [CommSemiring R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.natDegree ≤ 1

theorem Polynomial.Splits.degree_le_one_of_irreducible {R : Type u_1} [CommSemiring R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.degree ≤ 1

theorem Polynomial.Splits.comp_of_natDegree_le_one_of_invertible {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits

theorem Polynomial.Splits.comp_of_degree_le_one_of_invertible {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) (h : Invertible g.leadingCoeff) : (f.comp g).Splits

theorem Polynomial.Splits.comp_of_natDegree_le_one_of_monic {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) (h : g.Monic) : (f.comp g).Splits

theorem Polynomial.Splits.comp_of_degree_le_one_of_monic {R : Type u_1} [CommSemiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) (h : g.Monic) : (f.comp g).Splits

theorem Polynomial.Splits.comp_X_add_C {R : Type u_1} [CommSemiring R] {f : Polynomial R} (hf : f.Splits) (a : R) : (f.comp (X + C a)).Splits

theorem Polynomial.Splits.of_algHom {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (hf : (map (algebraMap R A) f).Splits) (e : A →ₐ[R] B) : (map (algebraMap R B) f).Splits

theorem Polynomial.Splits.of_isScalarTower {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} (B : Type u_3) [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (hf : (map (algebraMap R A) f).Splits) : (map (algebraMap R B) f).Splits

@[simp]

theorem Polynomial.Splits.X_sub_C {R : Type u_1} [Ring R] (a : R) : (X - C a).Splits

theorem Polynomial.Splits.neg {R : Type u_1} [Ring R] {f : Polynomial R} (hf : f.Splits) : (-f).Splits

@[simp]

theorem Polynomial.splits_neg_iff {R : Type u_1} [Ring R] {f : Polynomial R} : (-f).Splits ↔ f.Splits

theorem Polynomial.Splits.comp_neg_X {R : Type u_1} [Ring R] {f : Polynomial R} (hf : f.Splits) : (f.comp (-X)).Splits

theorem Polynomial.splits_iff_exists_multiset {R : Type u_1} [CommRing R] {f : Polynomial R} : f.Splits ↔ ∃ (m : Multiset R), f = C f.leadingCoeff * (Multiset.map (fun (x : R) => X - C x) m).prod

theorem Polynomial.Splits.exists_eval_eq_zero {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hf0 : f.degree ≠ 0) : ∃ (a : R), eval a f = 0

noncomputable def Polynomial.rootOfSplits {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hfd : f.degree ≠ 0) : R

Pick a root of a polynomial that splits.

@[simp]

theorem Polynomial.eval_rootOfSplits {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hfd : f.degree ≠ 0) : eval (rootOfSplits hf hfd) f = 0

theorem Polynomial.Splits.comp_X_sub_C {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (a : R) : (f.comp (X - C a)).Splits

theorem Polynomial.Splits.eq_prod_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f = C f.leadingCoeff * (Multiset.map (fun (x : R) => X - C x) f.roots).prod

theorem Polynomial.Splits.eq_prod_roots_of_monic {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f = (Multiset.map (fun (x : R) => X - C x) f.roots).prod

theorem Polynomial.Splits.eval_eq_prod_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (x : R) : eval x f = f.leadingCoeff * (Multiset.map (fun (x_1 : R) => x - x_1) f.roots).prod

theorem Polynomial.Splits.eval_eq_prod_roots_of_monic {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) (x : R) : eval x f = (Multiset.map (fun (x_1 : R) => x - x_1) f.roots).prod

theorem Polynomial.Splits.aeval_eq_prod_aroots {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [Algebra R A] [IsSimpleRing R] (hf : (map (algebraMap R A) f).Splits) (x : A) : (aeval x) f = (algebraMap R A) f.leadingCoeff * (Multiset.map (fun (x_1 : A) => x - x_1) (f.aroots A)).prod

theorem Polynomial.Splits.aeval_eq_prod_aroots_of_monic {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [Algebra R A] (hf : (map (algebraMap R A) f).Splits) (hm : f.Monic) (x : A) : (aeval x) f = (Multiset.map (fun (x_1 : A) => x - x_1) (f.aroots A)).prod

theorem Polynomial.Splits.eval_derivative {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : eval x (derivative f) = f.leadingCoeff * (Multiset.map (fun (a : R) => (Multiset.map (fun (x_1 : R) => x - x_1) (f.roots.erase a)).prod) f.roots).sum

theorem Polynomial.Splits.eval_root_derivative {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (hm : f.Monic) {x : R} (hx : x ∈ f.roots) : eval x (derivative f) = (Multiset.map (fun (x_1 : R) => x - x_1) (f.roots.erase x)).prod

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

theorem Polynomial.Splits.of_splits_map_of_injective {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_4} [CommRing S] [IsDomain S] {i : R →+* S} (hi : Function.Injective ⇑i) (hf : (map i f).Splits) : (∀ a ∈ (map i f).roots, a ∈ i.range) → f.Splits

theorem Polynomial.Splits.of_splits_map {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_4} [CommRing S] [IsDomain S] [IsSimpleRing R] (i : R →+* S) (hf : (map i f).Splits) (hi : ∀ a ∈ (map i f).roots, a ∈ i.range) : f.Splits

theorem Polynomial.Splits.mem_lift_of_roots_mem_range {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) {S : Type u_4} [Ring S] (i : S →+* R) (hr : ∀ a ∈ f.roots, a ∈ i.range) : f ∈ lifts i

theorem Polynomial.Splits.eq_X_sub_C_of_single_root {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) {x : R} (hr : f.roots = {x}) : f = C f.leadingCoeff * (X - C x)

theorem Polynomial.Splits.natDegree_eq_card_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.natDegree = f.roots.card

theorem Polynomial.Splits.degree_eq_card_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f ≠ 0) : f.degree = ↑f.roots.card

theorem Polynomial.splits_iff_card_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] : f.Splits ↔ f.roots.card = f.natDegree

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

theorem Polynomial.Splits.roots_ne_zero {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f.natDegree ≠ 0) : f.roots ≠ 0

theorem Polynomial.Splits.roots_map_of_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] {f : Polynomial R} (hf : f.Splits) {φ : R →+* S} (hφ : map φ f ≠ 0) : (map φ f).roots = Multiset.map (⇑φ) f.roots

theorem Polynomial.Splits.roots_map_of_injective {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] (hf : f.Splits) {i : R →+* S} (hi : Function.Injective ⇑i) : (map i f).roots = Multiset.map (⇑i) f.roots

theorem Polynomial.Splits.roots_map {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] [IsSimpleRing R] (hf : f.Splits) (i : R →+* S) : (map i f).roots = Multiset.map (⇑i) f.roots

@[deprecated Polynomial.Splits.roots_map (since := "2025-11-27")]

theorem Polynomial.Splits.map_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] [IsSimpleRing R] (hf : f.Splits) (i : R →+* S) : (map i f).roots = Multiset.map (⇑i) f.roots

Alias of Polynomial.Splits.roots_map.

theorem Polynomial.Splits.mem_range_of_isRoot {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] [IsSimpleRing R] (hf : f.Splits) (hf0 : f ≠ 0) {i : R →+* S} {x : S} (hx : (map i f).IsRoot x) : x ∈ i.range

theorem Polynomial.Splits.image_rootSet {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra R A] [Algebra R B] [IsSimpleRing A] (hf : (map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : ⇑g '' f.rootSet A = f.rootSet B

theorem Polynomial.Splits.adjoin_rootSet_eq_range {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra R A] [Algebra R B] [IsSimpleRing A] (hf : (map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤

theorem Polynomial.Splits.image_rootSet_of_map_ne_zero {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra R A] [Algebra R B] (hf : (map (algebraMap R A) f).Splits) (φ : A →ₐ[R] B) (hφ : map (algebraMap R B) f ≠ 0) : ⇑φ '' f.rootSet A = f.rootSet B

theorem Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod

theorem Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod

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

theorem Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.nextCoeff = -f.leadingCoeff * f.roots.sum

theorem Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.nextCoeff = -f.roots.sum

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

theorem Polynomial.splits_X_sub_C_mul_iff {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {a : R} : ((X - C a) * f).Splits ↔ f.Splits

theorem Polynomial.splits_mul_iff {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) : (f * g).Splits ↔ f.Splits ∧ g.Splits

theorem Polynomial.Splits.of_dvd {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hg : g.Splits) (hg₀ : g ≠ 0) (hfg : f ∣ g) : f.Splits

@[deprecated Polynomial.Splits.of_dvd (since := "2025-11-27")]

theorem Polynomial.Splits.splits_of_dvd {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hg : g.Splits) (hg₀ : g ≠ 0) (hfg : f ∣ g) : f.Splits

Alias of Polynomial.Splits.of_dvd.

theorem Polynomial.splits_prod_iff {R : Type u_1} [CommRing R] [IsDomain R] {ι : Type u_4} {f : ι → Polynomial R} {s : Finset ι} (hf : ∀ i ∈ s, f i ≠ 0) : (∏ x ∈ s, f x).Splits ↔ ∀ x ∈ s, (f x).Splits

@[deprecated "Use `Splits.degree_le_one_of_irreducible` instead." (since := "2026-01-13")]

theorem Polynomial.Splits.splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f = 0 ∨ ∀ {g : Polynomial R}, Irreducible g → g ∣ f → g.degree ≤ 1

theorem Polynomial.map_sub_sprod_roots_eq_prod_map_eval {R : Type u_1} [CommRing R] [IsDomain R] (s : Multiset R) (g : Polynomial R) (hg : g.Monic) (hg' : g.Splits) : (Multiset.map (fun (ij : R × R) => ij.1 - ij.2) (s ×ˢ g.roots)).prod = (Multiset.map (fun (x : R) => eval x g) s).prod

theorem Polynomial.map_sub_roots_sprod_eq_prod_map_eval {R : Type u_1} [CommRing R] [IsDomain R] (s : Multiset R) (g : Polynomial R) (hg : g.Monic) (hg' : g.Splits) : (Multiset.map (fun (ij : R × R) => ij.1 - ij.2) (g.roots ×ˢ s)).prod = (-1) ^ (s.card * g.roots.card) * (Multiset.map (fun (x : R) => eval x g) s).prod

theorem Polynomial.Splits.of_natDegree_le_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) : f.Splits

theorem Polynomial.Splits.of_natDegree_eq_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.natDegree = 1) : f.Splits

theorem Polynomial.Splits.of_degree_le_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree ≤ 1) : f.Splits

theorem Polynomial.Splits.of_degree_eq_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree = 1) : f.Splits

theorem Polynomial.Splits.dvd_of_roots_le_roots {R : Type u_1} [Field R] {f g : Polynomial R} (hp : f.Splits) (hp0 : f ≠ 0) (hq : f.roots ≤ g.roots) : f ∣ g

theorem Polynomial.Splits.dvd_iff_roots_le_roots {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hf0 : f ≠ 0) (hg0 : g ≠ 0) : f ∣ g ↔ f.roots ≤ g.roots

theorem Polynomial.Splits.comp_of_natDegree_le_one {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hg : g.natDegree ≤ 1) : (f.comp g).Splits

theorem Polynomial.Splits.comp_of_degree_le_one {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) : (f.comp g).Splits

theorem Polynomial.splits_iff_comp_splits_of_natDegree_eq_one {R : Type u_1} [Field R] {f g : Polynomial R} (hg : g.natDegree = 1) : f.Splits ↔ (f.comp g).Splits

theorem Polynomial.splits_iff_comp_splits_of_degree_eq_one {R : Type u_1} [Field R] {f g : Polynomial R} (hg : g.degree = 1) : f.Splits ↔ (f.comp g).Splits

theorem Polynomial.Splits.degree_eq_one_of_irreducible {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.degree = 1

theorem Polynomial.Splits.natDegree_eq_one_of_irreducible {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.natDegree = 1

theorem Polynomial.Splits.eval_derivative_eq_eval_mul_sum {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : eval x f ≠ 0) : eval x (derivative f) = eval x f * (Multiset.map (fun (z : R) => 1 / (x - z)) f.roots).sum

theorem Polynomial.Splits.eval_derivative_div_eval_of_ne_zero {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : eval x f ≠ 0) : eval x (derivative f) / eval x f = (Multiset.map (fun (z : R) => 1 / (x - z)) f.roots).sum

theorem Polynomial.Splits.mem_subfield_of_isRoot {R : Type u_1} [Field R] (F : Subfield R) {f : Polynomial ↥F} (hf : f.Splits) (hf0 : f ≠ 0) {x : R} (hx : (map F.subtype f).IsRoot x) : x ∈ F

theorem Polynomial.Splits.of_natDegree_eq_two {R : Type u_1} [Field R] {f : Polynomial R} {x : R} (h₁ : f.natDegree = 2) (h₂ : eval x f = 0) : f.Splits

A polynomial of degree 2 with a root splits.

theorem Polynomial.Splits.of_degree_eq_two {R : Type u_1} [Field R] {f : Polynomial R} {x : R} (h₁ : f.degree = 2) (h₂ : eval x f = 0) : f.Splits

@[deprecated "Use `Splits.degree_eq_one_of_irreducible` instead." (since := "2026-01-13")]

theorem Polynomial.splits_iff_splits {R : Type u_1} [Field R] {f : Polynomial R} : f.Splits ↔ f = 0 ∨ ∀ {g : Polynomial R}, Irreducible g → g ∣ f → g.degree = 1

@[deprecated Polynomial.Splits.zero (since := "2025-11-24")]

theorem Polynomial.splits_zero {R : Type u_1} [Semiring R] : Splits 0

Alias of Polynomial.Splits.zero.

@[deprecated "Use `Splits.C` instead." (since := "2025-11-24")]

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) : (map i f).Splits

@[deprecated Polynomial.Splits.C (since := "2025-11-24")]

theorem Polynomial.splits_C {R : Type u_1} [Semiring R] (a : R) : (C a).Splits

Alias of Polynomial.Splits.C.

@[deprecated Polynomial.Splits.of_degree_eq_one (since := "2025-11-24")]

theorem Polynomial.splits_of_map_degree_eq_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree = 1) : f.Splits

Alias of Polynomial.Splits.of_degree_eq_one.

@[deprecated Polynomial.Splits.of_degree_le_one (since := "2025-11-24")]

theorem Polynomial.splits_of_degree_le_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree ≤ 1) : f.Splits

Alias of Polynomial.Splits.of_degree_le_one.

@[deprecated Polynomial.Splits.of_degree_eq_one (since := "2025-11-24")]

theorem Polynomial.splits_of_degree_eq_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree = 1) : f.Splits

Alias of Polynomial.Splits.of_degree_eq_one.

@[deprecated Polynomial.Splits.of_natDegree_le_one (since := "2025-11-24")]

theorem Polynomial.splits_of_natDegree_le_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) : f.Splits

Alias of Polynomial.Splits.of_natDegree_le_one.

@[deprecated Polynomial.Splits.of_natDegree_eq_one (since := "2025-11-24")]

theorem Polynomial.splits_of_natDegree_eq_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.natDegree = 1) : f.Splits

Alias of Polynomial.Splits.of_natDegree_eq_one.

@[deprecated Polynomial.Splits.mul (since := "2025-11-25")]

theorem Polynomial.splits_mul {R : Type u_1} [Semiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.Splits) : (f * g).Splits

Alias of Polynomial.Splits.mul.

@[deprecated Polynomial.splits_mul_iff (since := "2025-11-25")]

theorem Polynomial.splits_of_splits_mul' {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) : (f * g).Splits ↔ f.Splits ∧ g.Splits

Alias of Polynomial.splits_mul_iff.

@[deprecated "Use `Polynomial.map_map` instead." (since := "2025-11-24")]

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} : (map j (map i f)).Splits ↔ (map (j.comp i) f).Splits

@[deprecated Polynomial.Splits.one (since := "2025-11-24")]

theorem Polynomial.splits_one {R : Type u_1} [Semiring R] : Splits 1

Alias of Polynomial.Splits.one.

@[deprecated Polynomial.Splits.X_sub_C (since := "2025-11-24")]

theorem Polynomial.splits_X_sub_C {R : Type u_1} [Ring R] (a : R) : (X - C a).Splits

Alias of Polynomial.Splits.X_sub_C.

@[deprecated Polynomial.Splits.X (since := "2025-11-24")]

theorem Polynomial.splits_X {R : Type u_1} [Semiring R] : X.Splits

Alias of Polynomial.Splits.X.

@[deprecated Polynomial.Splits.prod (since := "2025-11-24")]

theorem Polynomial.splits_prod {R : Type u_1} [CommSemiring R] {ι : Type u_2} {f : ι → Polynomial R} {s : Finset ι} (h : ∀ i ∈ s, (f i).Splits) : (∏ i ∈ s, f i).Splits

Alias of Polynomial.Splits.prod.

@[deprecated Polynomial.Splits.pow (since := "2025-11-24")]

theorem Polynomial.splits_pow {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) (n : ℕ) : (f ^ n).Splits

Alias of Polynomial.Splits.pow.

@[deprecated Polynomial.Splits.X_pow (since := "2025-11-24")]

theorem Polynomial.splits_X_pow {R : Type u_1} [Semiring R] (n : ℕ) : (X ^ n).Splits

Alias of Polynomial.Splits.X_pow.

@[deprecated "Use `Polynomial.map_id` instead." (since := "2025-11-24")]

theorem Polynomial.splits_id_iff_splits {K : Type v} {L : Type w} [CommRing K] [Field L] (i : K →+* L) {f : Polynomial K} : (map (RingHom.id L) (map i f)).Splits ↔ (map i f).Splits

@[deprecated Polynomial.Splits.comp_of_degree_le_one (since := "2025-11-25")]

theorem Polynomial.Splits.comp_of_map_degree_le_one {R : Type u_1} [Field R] {f g : Polynomial R} (hf : f.Splits) (hg : g.degree ≤ 1) : (f.comp g).Splits

Alias of Polynomial.Splits.comp_of_degree_le_one.

@[deprecated Polynomial.Splits.exists_eval_eq_zero (since := "2025-12-01")]

theorem Polynomial.exists_root_of_splits' {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hf0 : f.degree ≠ 0) : ∃ (a : R), eval a f = 0

Alias of Polynomial.Splits.exists_eval_eq_zero.

@[deprecated Polynomial.Splits.roots_ne_zero (since := "2025-12-01")]

theorem Polynomial.roots_ne_zero_of_splits' {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f.natDegree ≠ 0) : f.roots ≠ 0

Alias of Polynomial.Splits.roots_ne_zero.

@[deprecated Polynomial.rootOfSplits (since := "2025-12-01")]

def Polynomial.rootOfSplits' {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hfd : f.degree ≠ 0) : R

Alias of Polynomial.rootOfSplits.

---

Pick a root of a polynomial that splits.

@[deprecated Polynomial.eval_rootOfSplits (since := "2025-12-01")]

theorem Polynomial.map_rootOfSplits' {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hfd : f.degree ≠ 0) : eval (rootOfSplits hf hfd) f = 0

Alias of Polynomial.eval_rootOfSplits.

@[deprecated Polynomial.Splits.natDegree_eq_card_roots (since := "2025-12-01")]

theorem Polynomial.natDegree_eq_card_roots' {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.natDegree = f.roots.card

Alias of Polynomial.Splits.natDegree_eq_card_roots.

@[deprecated Polynomial.Splits.degree_eq_card_roots (since := "2025-12-01")]

theorem Polynomial.degree_eq_card_roots' {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f ≠ 0) : f.degree = ↑f.roots.card

Alias of Polynomial.Splits.degree_eq_card_roots.

@[deprecated Polynomial.splits_iff_splits (since := "2025-11-30")]

theorem Polynomial.splits_iff {R : Type u_1} [Field R] {f : Polynomial R} : f.Splits ↔ f = 0 ∨ ∀ {g : Polynomial R}, Irreducible g → g ∣ f → g.degree = 1

This lemma is for polynomials over a field.

@[deprecated Polynomial.splits_iff_splits (since := "2025-11-30")]

theorem Polynomial.Splits.def {R : Type u_1} [Field R] {f : Polynomial R} : f.Splits ↔ f = 0 ∨ ∀ {g : Polynomial R}, Irreducible g → g ∣ f → g.degree = 1

This lemma is for polynomials over a field.

@[deprecated Polynomial.splits_mul_iff (since := "2025-11-25")]

theorem Polynomial.splits_of_splits_mul {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) : (f * g).Splits ↔ f.Splits ∧ g.Splits

Alias of Polynomial.splits_mul_iff.

@[deprecated Polynomial.Splits.of_dvd (since := "2025-11-25")]

theorem Polynomial.splits_of_splits_of_dvd {R : Type u_1} [CommRing R] {f g : Polynomial R} [IsDomain R] (hg : g.Splits) (hg₀ : g ≠ 0) (hfg : f ∣ g) : f.Splits

Alias of Polynomial.Splits.of_dvd.

@[deprecated "Use `Splits.of_dvd` directly." (since := "2025-11-30")]

theorem Polynomial.splits_of_splits_gcd_left {K : Type v} [Field K] [DecidableEq K] {f g : Polynomial K} (hf0 : f ≠ 0) (hf : f.Splits) : (EuclideanDomain.gcd f g).Splits

@[deprecated "Use `Splits.of_dvd` directly." (since := "2025-11-30")]

theorem Polynomial.splits_of_splits_gcd_right {K : Type v} [Field K] [DecidableEq K] {f g : Polynomial K} (hg0 : g ≠ 0) (hg : g.Splits) : (EuclideanDomain.gcd f g).Splits

@[deprecated Polynomial.Splits.degree_eq_one_of_irreducible (since := "2025-11-30")]

theorem Polynomial.degree_eq_one_of_irreducible_of_splits {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) (h : Irreducible f) : f.degree = 1

Alias of Polynomial.Splits.degree_eq_one_of_irreducible.

@[deprecated Polynomial.Splits.exists_eval_eq_zero (since := "2025-12-01")]

theorem Polynomial.exists_root_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hf0 : f.degree ≠ 0) : ∃ (a : R), eval a f = 0

Alias of Polynomial.Splits.exists_eval_eq_zero.

@[deprecated Polynomial.Splits.roots_ne_zero (since := "2025-12-01")]

theorem Polynomial.roots_ne_zero_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f.natDegree ≠ 0) : f.roots ≠ 0

Alias of Polynomial.Splits.roots_ne_zero.

@[deprecated Polynomial.eval_rootOfSplits (since := "2025-12-01")]

theorem Polynomial.map_rootOfSplits {R : Type u_1} [CommRing R] {f : Polynomial R} (hf : f.Splits) (hfd : f.degree ≠ 0) : eval (rootOfSplits hf hfd) f = 0

Alias of Polynomial.eval_rootOfSplits.

@[deprecated "`rootOfSplits'` is now deprecated." (since := "2025-12-01")]

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

rootOfSplits' is definitionally equal to rootOfSplits.

@[deprecated Polynomial.Splits.natDegree_eq_card_roots (since := "2025-11-30")]

theorem Polynomial.natDegree_eq_card_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.natDegree = f.roots.card

Alias of Polynomial.Splits.natDegree_eq_card_roots.

@[deprecated Polynomial.Splits.degree_eq_card_roots (since := "2025-11-30")]

theorem Polynomial.degree_eq_card_roots {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hf0 : f ≠ 0) : f.degree = ↑f.roots.card

Alias of Polynomial.Splits.degree_eq_card_roots.

@[deprecated Polynomial.Splits.map_roots (since := "2025-12-02")]

theorem Polynomial.roots_map {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] {S : Type u_4} [CommRing S] [IsDomain S] [IsSimpleRing R] (hf : f.Splits) (i : R →+* S) : (map i f).roots = Multiset.map (⇑i) f.roots

Alias of Polynomial.Splits.roots_map.

---

Alias of Polynomial.Splits.roots_map.

@[deprecated Polynomial.Splits.image_rootSet (since := "2025-12-02")]

theorem Polynomial.image_rootSet {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra R A] [Algebra R B] [IsSimpleRing A] (hf : (map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : ⇑g '' f.rootSet A = f.rootSet B

Alias of Polynomial.Splits.image_rootSet.

@[deprecated Polynomial.Splits.adjoin_rootSet_eq_range (since := "2025-12-06")]

theorem Polynomial.adjoin_rootSet_eq_range {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra R A] [Algebra R B] [IsSimpleRing A] (hf : (map (algebraMap R A) f).Splits) (g : A →ₐ[R] B) : Algebra.adjoin R (f.rootSet B) = g.range ↔ Algebra.adjoin R (f.rootSet A) = ⊤

Alias of Polynomial.Splits.adjoin_rootSet_eq_range.

@[deprecated Polynomial.Splits.eq_prod_roots (since := "2025-11-25")]

theorem Polynomial.eq_prod_roots_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f = C f.leadingCoeff * (Multiset.map (fun (x : R) => X - C x) f.roots).prod

Alias of Polynomial.Splits.eq_prod_roots.

@[deprecated Polynomial.Splits.eq_prod_roots (since := "2025-11-25")]

theorem Polynomial.eq_prod_roots_of_splits_id {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f = C f.leadingCoeff * (Multiset.map (fun (x : R) => X - C x) f.roots).prod

Alias of Polynomial.Splits.eq_prod_roots.

@[deprecated Polynomial.Splits.aeval_eq_prod_aroots (since := "2025-12-06")]

theorem Polynomial.aeval_eq_prod_aroots_sub_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [Algebra R A] [IsSimpleRing R] (hf : (map (algebraMap R A) f).Splits) (x : A) : (aeval x) f = (algebraMap R A) f.leadingCoeff * (Multiset.map (fun (x_1 : A) => x - x_1) (f.aroots A)).prod

Alias of Polynomial.Splits.aeval_eq_prod_aroots.

@[deprecated Polynomial.Splits.eval_eq_prod_roots (since := "2025-12-06")]

theorem Polynomial.eval_eq_prod_roots_sub_of_splits_id {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (x : R) : eval x f = f.leadingCoeff * (Multiset.map (fun (x_1 : R) => x - x_1) f.roots).prod

Alias of Polynomial.Splits.eval_eq_prod_roots.

@[deprecated Polynomial.Splits.eq_prod_roots_of_monic (since := "2025-12-02")]

theorem Polynomial.eq_prod_roots_of_monic_of_splits_id {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f = (Multiset.map (fun (x : R) => X - C x) f.roots).prod

Alias of Polynomial.Splits.eq_prod_roots_of_monic.

@[deprecated Polynomial.Splits.aeval_eq_prod_aroots_of_monic (since := "2025-12-06")]

theorem Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} {A : Type u_2} [CommRing A] [IsDomain A] [Algebra R A] (hf : (map (algebraMap R A) f).Splits) (hm : f.Monic) (x : A) : (aeval x) f = (Multiset.map (fun (x_1 : A) => x - x_1) (f.aroots A)).prod

Alias of Polynomial.Splits.aeval_eq_prod_aroots_of_monic.

@[deprecated Polynomial.Splits.eval_eq_prod_roots_of_monic (since := "2025-12-06")]

theorem Polynomial.eval_eq_prod_roots_sub_of_monic_of_splits_id {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) (x : R) : eval x f = (Multiset.map (fun (x_1 : R) => x - x_1) f.roots).prod

Alias of Polynomial.Splits.eval_eq_prod_roots_of_monic.

@[deprecated Polynomial.Splits.eq_X_sub_C_of_single_root (since := "2025-12-06")]

theorem Polynomial.eq_X_sub_C_of_splits_of_single_root {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) {x : R} (hr : f.roots = {x}) : f = C f.leadingCoeff * (X - C x)

Alias of Polynomial.Splits.eq_X_sub_C_of_single_root.

@[deprecated Polynomial.Splits.mem_lift_of_roots_mem_range (since := "2025-12-13")]

theorem Polynomial.mem_lift_of_splits_of_roots_mem_range {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) {S : Type u_4} [Ring S] (i : S →+* R) (hr : ∀ a ∈ f.roots, a ∈ i.range) : f ∈ lifts i

Alias of Polynomial.Splits.mem_lift_of_roots_mem_range.

@[deprecated Polynomial.Splits.of_natDegree_eq_two (since := "2025-12-13")]

theorem Polynomial.splits_of_natDegree_eq_two {R : Type u_1} [Field R] {f : Polynomial R} {x : R} (h₁ : f.natDegree = 2) (h₂ : eval x f = 0) : f.Splits

Alias of Polynomial.Splits.of_natDegree_eq_two.

---

A polynomial of degree 2 with a root splits.

@[deprecated Polynomial.Splits.of_degree_eq_two (since := "2025-12-13")]

theorem Polynomial.splits_of_degree_eq_two {R : Type u_1} [Field R] {f : Polynomial R} {x : R} (h₁ : f.degree = 2) (h₂ : eval x f = 0) : f.Splits

Alias of Polynomial.Splits.of_degree_eq_two.

@[deprecated Polynomial.splits_iff_exists_multiset (since := "2025-12-02")]

theorem Polynomial.splits_of_exists_multiset {R : Type u_1} [CommRing R] {f : Polynomial R} : f.Splits ↔ ∃ (m : Multiset R), f = C f.leadingCoeff * (Multiset.map (fun (x : R) => X - C x) m).prod

Alias of Polynomial.splits_iff_exists_multiset.

@[deprecated Polynomial.Splits.map (since := "2025-11-30")]

theorem Polynomial.splits_of_splits_id {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) {S : Type u_2} [Semiring S] (i : R →+* S) : (map i f).Splits

Alias of Polynomial.Splits.map.

@[deprecated Polynomial.Splits.of_splits_map (since := "2025-12-09")]

theorem Polynomial.splits_of_comp {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_4} [CommRing S] [IsDomain S] [IsSimpleRing R] (i : R →+* S) (hf : (map i f).Splits) (hi : ∀ a ∈ (map i f).roots, a ∈ i.range) : f.Splits

Alias of Polynomial.Splits.of_splits_map.

@[deprecated Polynomial.Splits.of_splits_map (since := "2025-12-09")]

theorem Polynomial.splits_id_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} {S : Type u_4} [CommRing S] [IsDomain S] [IsSimpleRing R] (i : R →+* S) (hf : (map i f).Splits) (hi : ∀ a ∈ (map i f).roots, a ∈ i.range) : f.Splits

Alias of Polynomial.Splits.of_splits_map.

@[deprecated Polynomial.Splits.map (since := "2025-12-09")]

theorem Polynomial.splits_comp_of_splits {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) {S : Type u_2} [Semiring S] (i : R →+* S) : (map i f).Splits

Alias of Polynomial.Splits.map.

@[deprecated Polynomial.Splits.of_algHom (since := "2025-12-13")]

theorem Polynomial.splits_of_algHom {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (hf : (map (algebraMap R A) f).Splits) (e : A →ₐ[R] B) : (map (algebraMap R B) f).Splits

Alias of Polynomial.Splits.of_algHom.

@[deprecated Polynomial.Splits.of_isScalarTower (since := "2025-12-13")]

theorem Polynomial.splits_of_isScalarTower {R : Type u_1} [CommSemiring R] {f : Polynomial R} {A : Type u_2} (B : Type u_3) [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (hf : (map (algebraMap R A) f).Splits) : (map (algebraMap R B) f).Splits

Alias of Polynomial.Splits.of_isScalarTower.

@[deprecated Polynomial.Splits.eval_derivative (since := "2025-12-08")]

theorem Polynomial.eval₂_derivative_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : eval x (derivative f) = f.leadingCoeff * (Multiset.map (fun (a : R) => (Multiset.map (fun (x_1 : R) => x - x_1) (f.roots.erase a)).prod) f.roots).sum

Alias of Polynomial.Splits.eval_derivative.

@[deprecated Polynomial.Splits.eval_derivative (since := "2025-12-08")]

theorem Polynomial.aeval_derivative_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : eval x (derivative f) = f.leadingCoeff * (Multiset.map (fun (a : R) => (Multiset.map (fun (x_1 : R) => x - x_1) (f.roots.erase a)).prod) f.roots).sum

Alias of Polynomial.Splits.eval_derivative.

@[deprecated Polynomial.Splits.eval_derivative (since := "2025-12-08")]

theorem Polynomial.eval_derivative_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : eval x (derivative f) = f.leadingCoeff * (Multiset.map (fun (a : R) => (Multiset.map (fun (x_1 : R) => x - x_1) (f.roots.erase a)).prod) f.roots).sum

Alias of Polynomial.Splits.eval_derivative.

@[deprecated Polynomial.Splits.eval_root_derivative (since := "2025-12-08")]

theorem Polynomial.aeval_root_derivative_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (hm : f.Monic) {x : R} (hx : x ∈ f.roots) : eval x (derivative f) = (Multiset.map (fun (x_1 : R) => x - x_1) (f.roots.erase x)).prod

Alias of Polynomial.Splits.eval_root_derivative.

---

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

@[deprecated Polynomial.Splits.eval_derivative_eq_eval_mul_sum (since := "2025-12-12")]

theorem Polynomial.eval_derivative_eq_eval_mul_sum_of_splits {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : eval x f ≠ 0) : eval x (derivative f) = eval x f * (Multiset.map (fun (z : R) => 1 / (x - z)) f.roots).sum

Alias of Polynomial.Splits.eval_derivative_eq_eval_mul_sum.

@[deprecated Polynomial.Splits.eval_derivative_div_eval_of_ne_zero (since := "2025-12-12")]

theorem Polynomial.eval_derivative_div_eval_of_ne_zero_of_splits {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : eval x f ≠ 0) : eval x (derivative f) / eval x f = (Multiset.map (fun (z : R) => 1 / (x - z)) f.roots).sum

Alias of Polynomial.Splits.eval_derivative_div_eval_of_ne_zero.

@[deprecated Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots (since := "2025-12-12")]

theorem Polynomial.coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod

Alias of Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots.

@[deprecated Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic (since := "2025-12-12")]

theorem Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod

Alias of Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic.

---

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

@[deprecated Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff (since := "2025-12-12")]

theorem Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) : f.nextCoeff = -f.leadingCoeff * f.roots.sum

Alias of Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff.

@[deprecated Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic (since := "2025-12-12")]

theorem Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.nextCoeff = -f.roots.sum

Alias of Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic.

---

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

@[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 {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.coeff 0 = (-1) ^ f.natDegree * f.roots.prod

Alias of Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic.

---

Alias of Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic.

---

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

@[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 {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] (hf : f.Splits) (hm : f.Monic) : f.nextCoeff = -f.roots.sum

Alias of Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic.

---

Alias of Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic.

---

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