Split polynomials

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

Main definitions

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

TODO

• Redefine Splits in terms of Factors and then deprecate Splits.

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

A polynomial Factors if it is a product of constant and monic linear polynomials. This will eventually replace Polynomial.Splits.

Equations

• f.Factors = (f ∈ Submonoid.closure ({x : Polynomial R | ∃ (a : R), Polynomial.C a = x} ∪ {x : Polynomial R | ∃ (a : R), Polynomial.X + Polynomial.C a = x}))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

See factors_iff_exists_multiset for the version with subtraction.

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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