Documentation

Mathlib.Algebra.Polynomial.Div

Division of univariate polynomials #

The main defs are divByMonic and modByMonic. The compatibility between these is given by modByMonic_add_div. We also define rootMultiplicity.

theorem Polynomial.X_dvd_iff {R : Type u} [Semiring R] {f : Polynomial R} :
Polynomial.X f f.coeff 0 = 0
theorem Polynomial.X_pow_dvd_iff {R : Type u} [Semiring R] {f : Polynomial R} {n : } :
Polynomial.X ^ n f d < n, f.coeff d = 0
theorem Polynomial.finiteMultiplicity_of_degree_pos_of_monic {R : Type u} [Semiring R] {p q : Polynomial R} (hp : 0 < p.degree) (hmp : p.Monic) (hq : q 0) :
@[deprecated Polynomial.finiteMultiplicity_of_degree_pos_of_monic]
theorem Polynomial.multiplicity_finite_of_degree_pos_of_monic {R : Type u} [Semiring R] {p q : Polynomial R} (hp : 0 < p.degree) (hmp : p.Monic) (hq : q 0) :

Alias of Polynomial.finiteMultiplicity_of_degree_pos_of_monic.

theorem Polynomial.div_wf_lemma {R : Type u} [Ring R] {p q : Polynomial R} (h : q.degree p.degree p 0) (hq : q.Monic) :
(p - q * (Polynomial.C p.leadingCoeff * Polynomial.X ^ (p.natDegree - q.natDegree))).degree < p.degree
@[irreducible]
noncomputable def Polynomial.divModByMonicAux {R : Type u} [Ring R] (_p : Polynomial R) {q : Polynomial R} :
q.MonicPolynomial R × Polynomial R

See divByMonic.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Polynomial.divByMonic {R : Type u} [Ring R] (p q : Polynomial R) :

    divByMonic gives the quotient of p by a monic polynomial q.

    Equations
    • p /ₘ q = if hq : q.Monic then (p.divModByMonicAux hq).1 else 0
    Instances For
      def Polynomial.modByMonic {R : Type u} [Ring R] (p q : Polynomial R) :

      modByMonic gives the remainder of p by a monic polynomial q.

      Equations
      • p %ₘ q = if hq : q.Monic then (p.divModByMonicAux hq).2 else p
      Instances For

        divByMonic gives the quotient of p by a monic polynomial q.

        Equations
        Instances For

          modByMonic gives the remainder of p by a monic polynomial q.

          Equations
          Instances For
            @[irreducible]
            theorem Polynomial.degree_modByMonic_lt {R : Type u} [Ring R] [Nontrivial R] (p : Polynomial R) {q : Polynomial R} (_hq : q.Monic) :
            (p %ₘ q).degree < q.degree
            theorem Polynomial.natDegree_modByMonic_lt {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmq : q.Monic) (hq : q 1) :
            (p %ₘ q).natDegree < q.natDegree
            @[simp]
            theorem Polynomial.zero_modByMonic {R : Type u} [Ring R] (p : Polynomial R) :
            0 %ₘ p = 0
            @[simp]
            theorem Polynomial.zero_divByMonic {R : Type u} [Ring R] (p : Polynomial R) :
            0 /ₘ p = 0
            @[simp]
            theorem Polynomial.modByMonic_zero {R : Type u} [Ring R] (p : Polynomial R) :
            p %ₘ 0 = p
            @[simp]
            theorem Polynomial.divByMonic_zero {R : Type u} [Ring R] (p : Polynomial R) :
            p /ₘ 0 = 0
            theorem Polynomial.divByMonic_eq_of_not_monic {R : Type u} [Ring R] {q : Polynomial R} (p : Polynomial R) (hq : ¬q.Monic) :
            p /ₘ q = 0
            theorem Polynomial.modByMonic_eq_of_not_monic {R : Type u} [Ring R] {q : Polynomial R} (p : Polynomial R) (hq : ¬q.Monic) :
            p %ₘ q = p
            theorem Polynomial.modByMonic_eq_self_iff {R : Type u} [Ring R] {p q : Polynomial R} [Nontrivial R] (hq : q.Monic) :
            p %ₘ q = p p.degree < q.degree
            theorem Polynomial.degree_modByMonic_le {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : q.Monic) :
            (p %ₘ q).degree q.degree
            theorem Polynomial.natDegree_modByMonic_le {R : Type u} [Ring R] (p : Polynomial R) {g : Polynomial R} (hg : g.Monic) :
            (p %ₘ g).natDegree g.natDegree
            theorem Polynomial.X_dvd_sub_C {R : Type u} [Ring R] {p : Polynomial R} :
            Polynomial.X p - Polynomial.C (p.coeff 0)
            @[irreducible]
            theorem Polynomial.modByMonic_eq_sub_mul_div {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (_hq : q.Monic) :
            p %ₘ q = p - q * (p /ₘ q)
            theorem Polynomial.modByMonic_add_div {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : q.Monic) :
            p %ₘ q + q * (p /ₘ q) = p
            theorem Polynomial.divByMonic_eq_zero_iff {R : Type u} [Ring R] {p q : Polynomial R} [Nontrivial R] (hq : q.Monic) :
            p /ₘ q = 0 p.degree < q.degree
            theorem Polynomial.degree_add_divByMonic {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) (h : q.degree p.degree) :
            q.degree + (p /ₘ q).degree = p.degree
            theorem Polynomial.degree_divByMonic_le {R : Type u} [Ring R] (p q : Polynomial R) :
            (p /ₘ q).degree p.degree
            theorem Polynomial.degree_divByMonic_lt {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hq : q.Monic) (hp0 : p 0) (h0q : 0 < q.degree) :
            (p /ₘ q).degree < p.degree
            theorem Polynomial.natDegree_divByMonic {R : Type u} [Ring R] (f : Polynomial R) {g : Polynomial R} (hg : g.Monic) :
            (f /ₘ g).natDegree = f.natDegree - g.natDegree
            theorem Polynomial.div_modByMonic_unique {R : Type u} [Ring R] {f g : Polynomial R} (q r : Polynomial R) (hg : g.Monic) (h : r + g * q = f r.degree < g.degree) :
            f /ₘ g = q f %ₘ g = r
            theorem Polynomial.map_mod_divByMonic {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) :
            theorem Polynomial.map_divByMonic {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) :
            theorem Polynomial.map_modByMonic {R : Type u} {S : Type v} [Ring R] {p q : Polynomial R} [Ring S] (f : R →+* S) (hq : q.Monic) :
            theorem Polynomial.modByMonic_eq_zero_iff_dvd {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) :
            p %ₘ q = 0 q p
            @[deprecated Polynomial.modByMonic_eq_zero_iff_dvd]
            theorem Polynomial.dvd_iff_modByMonic_eq_zero {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) :
            p %ₘ q = 0 q p

            Alias of Polynomial.modByMonic_eq_zero_iff_dvd.

            @[simp]
            theorem Polynomial.self_mul_modByMonic {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) :
            q * p %ₘ q = 0

            See Polynomial.mul_left_modByMonic for the other multiplication order. That version, unlike this one, requires commutativity.

            theorem Polynomial.map_dvd_map {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Injective f) {x y : Polynomial R} (hx : x.Monic) :
            @[simp]
            theorem Polynomial.modByMonic_one {R : Type u} [Ring R] (p : Polynomial R) :
            p %ₘ 1 = 0
            @[simp]
            theorem Polynomial.divByMonic_one {R : Type u} [Ring R] (p : Polynomial R) :
            p /ₘ 1 = p
            theorem Polynomial.sum_modByMonic_coeff {R : Type u} [Ring R] {p q : Polynomial R} (hq : q.Monic) {n : } (hn : q.degree n) :
            i : Fin n, (Polynomial.monomial i) ((p %ₘ q).coeff i) = p %ₘ q
            theorem Polynomial.mul_divByMonic_cancel_left {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmo : q.Monic) :
            q * p /ₘ q = p
            @[deprecated Polynomial.mul_divByMonic_cancel_left]
            theorem Polynomial.mul_div_mod_by_monic_cancel_left {R : Type u} [Ring R] (p : Polynomial R) {q : Polynomial R} (hmo : q.Monic) :
            q * p /ₘ q = p

            Alias of Polynomial.mul_divByMonic_cancel_left.

            theorem Polynomial.coeff_divByMonic_X_sub_C_rec {R : Type u} [Ring R] (p : Polynomial R) (a : R) (n : ) :
            (p /ₘ (Polynomial.X - Polynomial.C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (Polynomial.X - Polynomial.C a)).coeff (n + 1)
            theorem Polynomial.coeff_divByMonic_X_sub_C {R : Type u} [Ring R] (p : Polynomial R) (a : R) (n : ) :
            (p /ₘ (Polynomial.X - Polynomial.C a)).coeff n = iFinset.Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
            def Polynomial.decidableDvdMonic {R : Type u} [Ring R] {q : Polynomial R} [DecidableEq R] (p : Polynomial R) (hq : q.Monic) :

            An algorithm for deciding polynomial divisibility. The algorithm is "compute p %ₘ q and compare to 0". See polynomial.modByMonic for the algorithm that computes %ₘ.

            Equations
            Instances For
              theorem Polynomial.finiteMultiplicity_X_sub_C {R : Type u} [Ring R] {p : Polynomial R} (a : R) (h0 : p 0) :
              FiniteMultiplicity (Polynomial.X - Polynomial.C a) p
              @[deprecated Polynomial.finiteMultiplicity_X_sub_C]
              theorem Polynomial.multiplicity_X_sub_C_finite {R : Type u} [Ring R] {p : Polynomial R} (a : R) (h0 : p 0) :
              FiniteMultiplicity (Polynomial.X - Polynomial.C a) p

              Alias of Polynomial.finiteMultiplicity_X_sub_C.

              def Polynomial.rootMultiplicity {R : Type u} [Ring R] (a : R) (p : Polynomial R) :

              The largest power of X - C a which divides p. This could be computable via the divisibility algorithm Polynomial.decidableDvdMonic, as shown by Polynomial.rootMultiplicity_eq_nat_find_of_nonzero which has a computable RHS.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem Polynomial.rootMultiplicity_eq_multiplicity {R : Type u} [Ring R] [DecidableEq R] (p : Polynomial R) (a : R) :
                Polynomial.rootMultiplicity a p = if p = 0 then 0 else multiplicity (Polynomial.X - Polynomial.C a) p
                @[simp]
                theorem Polynomial.rootMultiplicity_C {R : Type u} [Ring R] (r a : R) :
                Polynomial.rootMultiplicity a (Polynomial.C r) = 0
                theorem Polynomial.pow_rootMultiplicity_dvd {R : Type u} [Ring R] (p : Polynomial R) (a : R) :
                (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p p
                theorem Polynomial.pow_mul_divByMonic_rootMultiplicity_eq {R : Type u} [Ring R] (p : Polynomial R) (a : R) :
                (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p * (p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p) = p
                theorem Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd {R : Type u} [Ring R] (p : Polynomial R) (hp : p 0) (a : R) :
                ∃ (q : Polynomial R), p = (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p * q ¬Polynomial.X - Polynomial.C a q
                @[simp]
                theorem Polynomial.modByMonic_X_sub_C_eq_C_eval {R : Type u} [CommRing R] (p : Polynomial R) (a : R) :
                p %ₘ (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
                theorem Polynomial.mul_divByMonic_eq_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
                (Polynomial.X - Polynomial.C a) * (p /ₘ (Polynomial.X - Polynomial.C a)) = p p.IsRoot a
                theorem Polynomial.dvd_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
                Polynomial.X - Polynomial.C a p p.IsRoot a
                theorem Polynomial.X_sub_C_dvd_sub_C_eval {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
                Polynomial.X - Polynomial.C a p - Polynomial.C (Polynomial.eval a p)
                theorem Polynomial.modByMonic_X {R : Type u} [CommRing R] (p : Polynomial R) :
                p %ₘ Polynomial.X = Polynomial.C (Polynomial.eval 0 p)
                theorem Polynomial.eval₂_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} {p q : Polynomial R} (hq : q.Monic) {x : S} (hx : Polynomial.eval₂ f x q = 0) :
                @[simp]
                theorem Polynomial.rootMultiplicity_eq_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} {x : R} :
                Polynomial.rootMultiplicity x p = 0 p.IsRoot xp = 0
                theorem Polynomial.rootMultiplicity_eq_zero {R : Type u} [CommRing R] {p : Polynomial R} {x : R} (h : ¬p.IsRoot x) :
                @[simp]
                theorem Polynomial.rootMultiplicity_pos' {R : Type u} [CommRing R] {p : Polynomial R} {x : R} :
                0 < Polynomial.rootMultiplicity x p p 0 p.IsRoot x
                theorem Polynomial.rootMultiplicity_pos {R : Type u} [CommRing R] {p : Polynomial R} (hp : p 0) {x : R} :
                theorem Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero {R : Type u} [CommRing R] {p : Polynomial R} (a : R) (hp : p 0) :
                Polynomial.eval a (p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p) 0
                @[simp]
                theorem Polynomial.mul_self_modByMonic {R : Type u} [CommRing R] {p q : Polynomial R} (hq : q.Monic) :
                p * q %ₘ q = 0

                See Polynomial.mul_right_modByMonic for the other multiplication order. This version, unlike that one, requires commutativity.

                theorem Polynomial.modByMonic_eq_of_dvd_sub {R : Type u} [CommRing R] {p₁ p₂ q : Polynomial R} (hq : q.Monic) (h : q p₁ - p₂) :
                p₁ %ₘ q = p₂ %ₘ q
                theorem Polynomial.add_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (p₁ p₂ : Polynomial R) :
                (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
                theorem Polynomial.neg_modByMonic {R : Type u} [CommRing R] (p q : Polynomial R) :
                -p %ₘ q = -(p %ₘ q)
                theorem Polynomial.sub_modByMonic {R : Type u} [CommRing R] (p₁ p₂ q : Polynomial R) :
                (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q
                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.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

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

                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

                See Polynomial.rootMultiplicity_eq_natTrailingDegree for the general case.

                theorem Polynomial.leadingCoeff_divByMonic_of_monic {R : Type u} [CommRing R] {p 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.degree_eq_one_of_irreducible_of_root {R : Type u} [CommRing R] {p : Polynomial R} [IsDomain R] (hi : Irreducible p) {x : R} (hx : p.IsRoot x) :
                p.degree = 1
                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 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 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 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 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 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 q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (hdiv : p q) (hdeg : q.natDegree p.natDegree) :
                q = p