Documentation

Mathlib.Algebra.Polynomial.Factors

Split polynomials #

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

Main definitions #

source
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. This will eventually replace Polynomial.Splits.

Equations
Instances For
    source
    @[simp]
    theorem Polynomial.Splits.C {R : Type u_1} [Semiring R] (a : R) :
    (C a).Splits
    source
    @[simp]
    theorem Polynomial.Splits.zero {R : Type u_1} [Semiring R] :
    Splits 0
    source
    @[simp]
    theorem Polynomial.Splits.one {R : Type u_1} [Semiring R] :
    Splits 1
    source
    @[simp]
    theorem Polynomial.Splits.X_add_C {R : Type u_1} [Semiring R] (a : R) :
    (X + C a).Splits
    source
    @[simp]
    theorem Polynomial.Splits.X {R : Type u_1} [Semiring R] :
    X.Splits
    source
    @[simp]
    theorem Polynomial.Splits.mul {R : Type u_1} [Semiring R] {f g : Polynomial R} (hf : f.Splits) (hg : g.Splits) :
    (f * g).Splits
    source
    theorem Polynomial.Splits.C_mul {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) (a : R) :
    (C a * f).Splits
    source
    @[simp]
    theorem Polynomial.Splits.listProd {R : Type u_1} [Semiring R] {l : List (Polynomial R)} (h : ∀ f ∈ l, f.Splits) :
    l.prod.Splits
    source
    @[simp]
    theorem Polynomial.Splits.pow {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.Splits) (n : ℕ) :
    (f ^ n).Splits
    source
    theorem Polynomial.Splits.X_pow {R : Type u_1} [Semiring R] (n : ℕ) :
    (X ^ n).Splits
    source
    theorem Polynomial.Splits.C_mul_X_pow {R : Type u_1} [Semiring R] (a : R) (n : ℕ) :
    (C a * X ^ n).Splits
    source
    @[simp]
    theorem Polynomial.Splits.monomial {R : Type u_1} [Semiring R] (n : ℕ) (a : R) :
    ((Polynomial.monomial n) a).Splits
    source
    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
    source
    theorem Polynomial.splits_of_natDegree_eq_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.natDegree = 0) :
    f.Splits
    source
    theorem Polynomial.splits_of_degree_le_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f.degree ≤ 0) :
    f.Splits
    source
    @[simp]
    theorem Polynomial.Splits.multisetProd {R : Type u_1} [CommSemiring R] {m : Multiset (Polynomial R)} (hm : ∀ f ∈ m, f.Splits) :
    m.prod.Splits
    source
    @[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
    source
    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.

    source
    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
    source
    @[simp]
    theorem Polynomial.Splits.X_sub_C {R : Type u_1} [Ring R] (a : R) :
    (X - C a).Splits
    source
    theorem Polynomial.Splits.neg {R : Type u_1} [Ring R] {f : Polynomial R} (hf : f.Splits) :
    (-f).Splits
    source
    @[simp]
    theorem Polynomial.splits_neg_iff {R : Type u_1} [Ring R] {f : Polynomial R} :
    (-f).Splits ↔ f.Splits
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    theorem Polynomial.Splits.of_natDegree_le_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.natDegree ≤ 1) :
    f.Splits
    source
    theorem Polynomial.Splits.of_natDegree_eq_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.natDegree = 1) :
    f.Splits
    source
    theorem Polynomial.Splits.of_degree_le_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree ≤ 1) :
    f.Splits
    source
    theorem Polynomial.Splits.of_degree_eq_one {R : Type u_1} [DivisionSemiring R] {f : Polynomial R} (hf : f.degree = 1) :
    f.Splits
    source
    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