Documentation

Mathlib.Algebra.Polynomial.RingDivision

Theory of univariate polynomials #

We prove basic results about univariate polynomials.

theorem Polynomial.Monic.comp {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (h : q.natDegree 0) :
(p.comp q).Monic
theorem Polynomial.Monic.comp_X_add_C {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (r : R) :
(p.comp (Polynomial.X + Polynomial.C r)).Monic
theorem Polynomial.natDegree_pos_of_aeval_root {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p 0) {z : S} (hz : (Polynomial.aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0x = 0) :
0 < p.natDegree
theorem Polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p 0) {z : S} (hz : (Polynomial.aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0x = 0) :
0 < p.degree
theorem Polynomial.modByMonic_eq_of_dvd_sub {R : Type u} [CommRing R] {q : Polynomial R} (hq : q.Monic) {p₁ : Polynomial R} {p₂ : Polynomial R} (h : q p₁ - p₂) :
p₁ %ₘ q = p₂ %ₘ q
theorem Polynomial.add_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (p₁ : Polynomial R) (p₂ : Polynomial R) :
(p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
theorem Polynomial.smul_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (c : R) (p : Polynomial R) :
c p %ₘ q = c (p %ₘ q)
@[simp]
theorem Polynomial.modByMonicHom_apply {R : Type u} [CommRing R] (q : Polynomial R) (p : Polynomial R) :
q.modByMonicHom p = p %ₘ q

_ %ₘ q as an R-linear map.

Equations
  • q.modByMonicHom = { toFun := fun (p : Polynomial R) => p %ₘ q, map_add' := , map_smul' := }
Instances For
    theorem Polynomial.neg_modByMonic {R : Type u} [CommRing R] (p : Polynomial R) (mod : Polynomial R) :
    -p %ₘ mod = -(p %ₘ mod)
    theorem Polynomial.sub_modByMonic {R : Type u} [CommRing R] (a : Polynomial R) (b : Polynomial R) (mod : Polynomial R) :
    (a - b) %ₘ mod = a %ₘ mod - b %ₘ mod
    theorem Polynomial.aeval_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {p : Polynomial R} {q : Polynomial R} (hq : q.Monic) {x : S} (hx : (Polynomial.aeval x) q = 0) :
    theorem Polynomial.natDegree_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (hp : p 0) (hq : q 0) :
    (p * q).natDegree = p.natDegree + q.natDegree
    theorem Polynomial.trailingDegree_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} :
    (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
    @[simp]
    theorem Polynomial.natDegree_pow {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (n : ) :
    (p ^ n).natDegree = n * p.natDegree
    theorem Polynomial.degree_le_mul_left {R : Type u} [Semiring R] [NoZeroDivisors R] {q : Polynomial R} (p : Polynomial R) (hq : q 0) :
    p.degree (p * q).degree
    theorem Polynomial.natDegree_le_of_dvd {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h1 : p q) (h2 : q 0) :
    p.natDegree q.natDegree
    theorem Polynomial.degree_le_of_dvd {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h1 : p q) (h2 : q 0) :
    p.degree q.degree
    theorem Polynomial.eq_zero_of_dvd_of_degree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h₁ : p q) (h₂ : q.degree < p.degree) :
    q = 0
    theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h₁ : p q) (h₂ : q.natDegree < p.natDegree) :
    q = 0
    theorem Polynomial.not_dvd_of_degree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h0 : q 0) (hl : q.degree < p.degree) :
    ¬p q
    theorem Polynomial.not_dvd_of_natDegree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h0 : q 0) (hl : q.natDegree < p.natDegree) :
    ¬p q
    theorem Polynomial.natDegree_sub_eq_of_prod_eq {R : Type u} [Semiring R] [NoZeroDivisors R] {p₁ : Polynomial R} {p₂ : Polynomial R} {q₁ : Polynomial R} {q₂ : Polynomial R} (hp₁ : p₁ 0) (hq₁ : q₁ 0) (hp₂ : p₂ 0) (hq₂ : q₂ 0) (h_eq : p₁ * q₂ = p₂ * q₁) :
    p₁.natDegree - q₁.natDegree = p₂.natDegree - q₂.natDegree

    This lemma is useful for working with the intDegree of a rational function.

    theorem Polynomial.natDegree_eq_zero_of_isUnit {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} (h : IsUnit p) :
    p.natDegree = 0
    theorem Polynomial.degree_eq_zero_of_isUnit {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} [Nontrivial R] (h : IsUnit p) :
    p.degree = 0
    @[simp]
    theorem Polynomial.degree_coe_units {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) :
    (↑u).degree = 0
    theorem Polynomial.isUnit_iff {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} :
    IsUnit p ∃ (r : R), IsUnit r Polynomial.C r = p

    Characterization of a unit of a polynomial ring over an integral domain R. See Polynomial.isUnit_iff_coeff_isUnit_isNilpotent when R is a commutative ring.

    theorem Polynomial.not_isUnit_of_degree_pos {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < p.degree) :
    theorem Polynomial.not_isUnit_of_natDegree_pos {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < p.natDegree) :
    theorem Polynomial.irreducible_of_monic {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hp1 : p 1) :
    Irreducible p ∀ (f g : Polynomial R), f.Monicg.Monicf * g = pf = 1 g = 1
    theorem Polynomial.Monic.irreducible_iff_natDegree {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) :
    Irreducible p p 1 ∀ (f g : Polynomial R), f.Monicg.Monicf * g = pf.natDegree = 0 g.natDegree = 0
    theorem Polynomial.Monic.irreducible_iff_natDegree' {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) :
    Irreducible p p 1 ∀ (f g : Polynomial R), f.Monicg.Monicf * g = pg.natDegreeFinset.Ioc 0 (p.natDegree / 2)
    theorem Polynomial.Monic.irreducible_iff_lt_natDegree_lt {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hp1 : p 1) :
    Irreducible p ∀ (q : Polynomial R), q.Monicq.natDegree Finset.Ioc 0 (p.natDegree / 2)¬q p

    Alternate phrasing of Polynomial.Monic.irreducible_iff_natDegree' where we only have to check one divisor at a time.

    theorem Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hm : p.Monic) (hnd : p.natDegree = 2) :
    ¬Irreducible p ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ p.coeff 1 = c₁ + c₂
    theorem Polynomial.root_mul {R : Type u} {a : R} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} :
    (p * q).IsRoot a p.IsRoot a q.IsRoot a
    theorem Polynomial.root_or_root_of_root_mul {R : Type u} {a : R} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} {q : Polynomial R} (h : (p * q).IsRoot a) :
    p.IsRoot a q.IsRoot a
    Equations
    • =
    theorem Polynomial.Monic.C_dvd_iff_isUnit {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) {a : R} :
    Polynomial.C a p IsUnit a
    theorem Polynomial.Monic.natDegree_pos {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) :
    0 < p.natDegree p 1
    theorem Polynomial.Monic.degree_pos {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) :
    0 < p.degree p 1
    theorem Polynomial.Monic.degree_pos_of_not_isUnit {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) (hu : ¬IsUnit p) :
    0 < p.degree
    theorem Polynomial.Monic.natDegree_pos_of_not_isUnit {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) (hu : ¬IsUnit p) :
    0 < p.natDegree
    theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic {R : Type u} [CommSemiring R] {a : Polynomial R} {p : Polynomial R} (hp : p.Monic) (ha : ¬IsUnit a) (hap : a p) :
    0 < a.degree
    theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic {R : Type u} [CommSemiring R] {a : Polynomial R} {p : Polynomial R} (hp : p.Monic) (ha : ¬IsUnit a) (hap : a p) :
    0 < a.natDegree
    @[irreducible]
    theorem Polynomial.eq_zero_of_mul_eq_zero_of_smul {R : Type u} [CommSemiring R] (P : Polynomial R) (h : ∀ (r : R), r P = 0r = 0) (Q : Polynomial R) :
    P * Q = 0Q = 0
    theorem Polynomial.nmem_nonZeroDivisors_iff {R : Type u} [CommSemiring R] {P : Polynomial R} :
    PnonZeroDivisors (Polynomial R) ∃ (a : R), a 0 a P = 0

    McCoy theorem: a polynomial P : R[X] is a zerodivisor if and only if there is a : R such that a ≠ 0 and a • P = 0.

    theorem Polynomial.mem_nonZeroDivisors_iff {R : Type u} [CommSemiring R] {P : Polynomial R} :
    P nonZeroDivisors (Polynomial R) ∀ (a : R), a P = 0a = 0
    theorem Polynomial.le_rootMultiplicity_iff {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p 0) {a : R} {n : } :
    n Polynomial.rootMultiplicity a p (Polynomial.X - Polynomial.C a) ^ n p

    The multiplicity of a as root of a nonzero polynomial p is at least n iff (X - a) ^ n divides p.

    theorem Polynomial.rootMultiplicity_le_iff {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p 0) (a : R) (n : ) :
    Polynomial.rootMultiplicity a p n ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) p
    theorem Polynomial.pow_rootMultiplicity_not_dvd {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p 0) (a : R) :
    ¬(Polynomial.X - Polynomial.C a) ^ (Polynomial.rootMultiplicity a p + 1) p
    theorem Polynomial.X_sub_C_pow_dvd_iff {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : } :
    (Polynomial.X - Polynomial.C t) ^ n p Polynomial.X ^ n p.comp (Polynomial.X + Polynomial.C t)
    theorem Polynomial.comp_X_add_C_eq_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} (t : R) :
    p.comp (Polynomial.X + Polynomial.C t) = 0 p = 0
    theorem Polynomial.comp_X_add_C_ne_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} (t : R) :
    p.comp (Polynomial.X + Polynomial.C t) 0 p 0
    theorem Polynomial.rootMultiplicity_eq_rootMultiplicity {R : Type u} [CommRing R] {p : Polynomial R} {t : R} :
    Polynomial.rootMultiplicity t p = Polynomial.rootMultiplicity 0 (p.comp (Polynomial.X + Polynomial.C t))
    theorem Polynomial.rootMultiplicity_eq_natTrailingDegree {R : Type u} [CommRing R] {p : Polynomial R} {t : R} :
    Polynomial.rootMultiplicity t p = (p.comp (Polynomial.X + Polynomial.C t)).natTrailingDegree
    theorem Polynomial.eval_divByMonic_eq_trailingCoeff_comp {R : Type u} [CommRing R] {p : Polynomial R} {t : R} :
    Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p) = (p.comp (Polynomial.X + Polynomial.C t)).trailingCoeff
    theorem Polynomial.rootMultiplicity_mul_X_sub_C_pow {R : Type u} [CommRing R] {p : Polynomial R} {a : R} {n : } (h : p 0) :
    Polynomial.rootMultiplicity a (p * (Polynomial.X - Polynomial.C a) ^ n) = Polynomial.rootMultiplicity a p + n
    theorem Polynomial.rootMultiplicity_X_sub_C_pow {R : Type u} [CommRing R] [Nontrivial R] (a : R) (n : ) :
    Polynomial.rootMultiplicity a ((Polynomial.X - Polynomial.C a) ^ n) = n

    The multiplicity of a as root of (X - a) ^ n is n.

    theorem Polynomial.rootMultiplicity_X_sub_C_self {R : Type u} [CommRing R] [Nontrivial R] {x : R} :
    Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C x) = 1
    theorem Polynomial.rootMultiplicity_X_sub_C {R : Type u} [CommRing R] [Nontrivial R] [DecidableEq R] {x : R} {y : R} :
    Polynomial.rootMultiplicity x (Polynomial.X - Polynomial.C y) = if x = y then 1 else 0

    The multiplicity of p + q is at least the minimum of the multiplicities.

    theorem Polynomial.rootMultiplicity_mul' {R : Type u} [CommRing R] {p : Polynomial R} {q : Polynomial R} {x : R} (hpq : Polynomial.eval x (p /ₘ (Polynomial.X - Polynomial.C x) ^ Polynomial.rootMultiplicity x p) * Polynomial.eval x (q /ₘ (Polynomial.X - Polynomial.C x) ^ Polynomial.rootMultiplicity x q) 0) :
    theorem Polynomial.Monic.comp_X_sub_C {R : Type u} [CommRing R] {p : Polynomial R} (hp : p.Monic) (r : R) :
    (p.comp (Polynomial.X - Polynomial.C r)).Monic
    @[simp]
    theorem Polynomial.natDegree_coe_units {R : Type u} [CommRing R] [IsDomain R] (u : (Polynomial R)ˣ) :
    (↑u).natDegree = 0
    theorem Polynomial.coeff_coe_units_zero_ne_zero {R : Type u} [CommRing R] [IsDomain R] (u : (Polynomial R)ˣ) :
    (↑u).coeff 0 0
    theorem Polynomial.degree_eq_degree_of_associated {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (h : Associated p q) :
    p.degree = q.degree
    theorem Polynomial.degree_eq_one_of_irreducible_of_root {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hi : Irreducible p) {x : R} (hx : p.IsRoot x) :
    p.degree = 1
    theorem Polynomial.leadingCoeff_divByMonic_of_monic {R : Type u} [CommRing R] {p : Polynomial R} {q : Polynomial R} (hmonic : q.Monic) (hdegree : q.degree p.degree) :
    (p /ₘ q).leadingCoeff = p.leadingCoeff

    Division by a monic polynomial doesn't change the leading coefficient.

    theorem Polynomial.leadingCoeff_divByMonic_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) (hp : p.degree 0) (a : R) :
    (p /ₘ (Polynomial.X - Polynomial.C a)).leadingCoeff = p.leadingCoeff
    theorem Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (hpq : p q) (h₁ : q.natDegree p.natDegree) (h₂ : p.leadingCoeff = q.leadingCoeff) :
    p = q
    theorem Polynomial.associated_of_dvd_of_natDegree_le_of_leadingCoeff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} (hpq : p q) (h₁ : q.natDegree p.natDegree) (h₂ : q.leadingCoeff p.leadingCoeff) :
    theorem Polynomial.associated_of_dvd_of_natDegree_le {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hpq : p q) (hq : q 0) (h₁ : q.natDegree p.natDegree) :
    theorem Polynomial.associated_of_dvd_of_degree_eq {K : Type u_1} [Field K] {p : Polynomial K} {q : Polynomial K} (hpq : p q) (h₁ : p.degree = q.degree) :
    theorem Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [CommRing R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hdiv : p q) (hdeg : q.natDegree p.natDegree) :
    q = Polynomial.C q.leadingCoeff * p
    theorem Polynomial.eq_of_monic_of_dvd_of_natDegree_le {R : Type u_1} [CommRing R] {p : Polynomial R} {q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (hdiv : p q) (hdeg : q.natDegree p.natDegree) :
    q = p
    theorem Polynomial.prime_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) :
    Prime (Polynomial.X - Polynomial.C r)
    theorem Polynomial.prime_X {R : Type u} [CommRing R] [IsDomain R] :
    Prime Polynomial.X
    theorem Polynomial.Monic.prime_of_degree_eq_one {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp1 : p.degree = 1) (hm : p.Monic) :
    theorem Polynomial.irreducible_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) :
    Irreducible (Polynomial.X - Polynomial.C r)
    theorem Polynomial.irreducible_X {R : Type u} [CommRing R] [IsDomain R] :
    Irreducible Polynomial.X
    theorem Polynomial.Monic.irreducible_of_degree_eq_one {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp1 : p.degree = 1) (hm : p.Monic) :
    @[simp]
    theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card {R : Type u} [CommRing R] [IsDomain R] (s : Multiset R) :
    (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s).prod.natDegree = Multiset.card s
    theorem Polynomial.units_coeff_zero_smul {R : Type u} [CommRing R] [IsDomain R] (c : (Polynomial R)ˣ) (p : Polynomial R) :
    (↑c).coeff 0 p = c * p
    theorem Polynomial.comp_eq_zero_iff {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} {q : Polynomial R} :
    p.comp q = 0 p = 0 Polynomial.eval (q.coeff 0) p = 0 q = Polynomial.C (q.coeff 0)
    theorem Polynomial.aeval_ne_zero_of_isCoprime {S : Type v} {R : Type u_1} [CommSemiring R] [Nontrivial S] [Semiring S] [Algebra R S] {p : Polynomial R} {q : Polynomial R} (h : IsCoprime p q) (s : S) :
    theorem Polynomial.isCoprime_X_sub_C_of_isUnit_sub {R : Type u_1} [CommRing R] {a : R} {b : R} (h : IsUnit (a - b)) :
    IsCoprime (Polynomial.X - Polynomial.C a) (Polynomial.X - Polynomial.C b)
    theorem Polynomial.pairwise_coprime_X_sub_C {K : Type u_1} [Field K] {I : Type v} {s : IK} (H : Function.Injective s) :
    Pairwise (IsCoprime on fun (i : I) => Polynomial.X - Polynomial.C (s i))
    @[irreducible]
    theorem Polynomial.exists_multiset_roots {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {p : Polynomial R} :
    p 0∃ (s : Multiset R), (Multiset.card s) p.degree ∀ (a : R), Multiset.count a s = Polynomial.rootMultiplicity a p
    theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map {R : Type u} {S : Type v} [Semiring R] [CommRing S] [IsDomain S] (φ : R →+* S) {f : Polynomial R} (hf : IsUnit f.leadingCoeff) (H : IsUnit (Polynomial.map φ f)) :
    theorem Polynomial.Monic.irreducible_of_irreducible_map {R : Type u} {S : Type v} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] (φ : R →+* S) (f : Polynomial R) (h_mon : f.Monic) (h_irr : Irreducible (Polynomial.map φ f)) :

    A polynomial over an integral domain R is irreducible if it is monic and irreducible after mapping into an integral domain S.

    A special case of this lemma is that a polynomial over is irreducible if it is monic and irreducible over ℤ/pℤ for some prime p.