Documentation

Mathlib.Data.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} [CommSemiring R] {f : Polynomial R} :
Polynomial.X f Polynomial.coeff f 0 = 0
theorem Polynomial.X_pow_dvd_iff {R : Type u} [CommSemiring R] {f : Polynomial R} {n : } :
Polynomial.X ^ n f ∀ (d : ), d < nPolynomial.coeff f d = 0
noncomputable def Polynomial.divModByMonicAux {R : Type u} [Ring R] (_p : Polynomial R) {q : 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 : Polynomial R) (q : Polynomial R) :

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

    Equations
    Instances For
      def Polynomial.modByMonic {R : Type u} [Ring R] (p : Polynomial R) (q : Polynomial R) :

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

      Equations
      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
            @[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.X_dvd_sub_C {R : Type u} [CommRing R] {p : Polynomial R} :
            Polynomial.X p - Polynomial.C (Polynomial.coeff p 0)
            theorem Polynomial.modByMonic_eq_sub_mul_div {R : Type u} [CommRing R] (p : Polynomial R) {q : Polynomial R} (_hq : Polynomial.Monic q) :
            p %ₘ q = p - q * (p /ₘ q)
            theorem Polynomial.modByMonic_add_div {R : Type u} [CommRing R] (p : Polynomial R) {q : Polynomial R} (hq : Polynomial.Monic q) :
            p %ₘ q + q * (p /ₘ q) = p
            theorem Polynomial.div_modByMonic_unique {R : Type u} [CommRing R] {f : Polynomial R} {g : Polynomial R} (q : Polynomial R) (r : Polynomial R) (hg : Polynomial.Monic g) (h : r + g * q = f Polynomial.degree r < Polynomial.degree g) :
            f /ₘ g = q f %ₘ g = r
            theorem Polynomial.map_divByMonic {R : Type u} {S : Type v} [CommRing R] {p : Polynomial R} {q : Polynomial R} [CommRing S] (f : R →+* S) (hq : Polynomial.Monic q) :
            theorem Polynomial.map_modByMonic {R : Type u} {S : Type v} [CommRing R] {p : Polynomial R} {q : Polynomial R} [CommRing S] (f : R →+* S) (hq : Polynomial.Monic q) :
            theorem Polynomial.map_dvd_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Injective f) {x : Polynomial R} {y : Polynomial R} (hx : Polynomial.Monic x) :
            @[simp]
            theorem Polynomial.modByMonic_one {R : Type u} [CommRing R] (p : Polynomial R) :
            p %ₘ 1 = 0
            @[simp]
            theorem Polynomial.divByMonic_one {R : Type u} [CommRing R] (p : Polynomial R) :
            p /ₘ 1 = p
            @[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 Polynomial.IsRoot p a
            theorem Polynomial.dvd_iff_isRoot {R : Type u} {a : R} [CommRing R] {p : Polynomial R} :
            Polynomial.X - Polynomial.C a p Polynomial.IsRoot p 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.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero {R : Type u} {a : R} [CommRing R] {b : Polynomial R} {P : Polynomial (Polynomial R)} :
            P Ideal.span {Polynomial.C (Polynomial.X - Polynomial.C a), Polynomial.X - Polynomial.C b} Polynomial.eval a (Polynomial.eval b P) = 0
            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 : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) {x : S} (hx : Polynomial.eval₂ f x q = 0) :
            theorem Polynomial.sum_modByMonic_coeff {R : Type u} [CommRing R] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) {n : } (hn : Polynomial.degree q n) :
            (Finset.sum Finset.univ fun i => ↑(Polynomial.monomial i) (Polynomial.coeff (p %ₘ q) i)) = p %ₘ q
            theorem Polynomial.sub_dvd_eval_sub {R : Type u} [CommRing R] (a : R) (b : R) (p : Polynomial R) :
            theorem Polynomial.ker_evalRingHom {R : Type u} [CommRing R] (x : R) :
            RingHom.ker (Polynomial.evalRingHom x) = Ideal.span {Polynomial.X - Polynomial.C x}

            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.multiplicity_X_sub_C_finite {R : Type u} [CommRing R] {p : Polynomial R} (a : R) (h0 : p 0) :
              multiplicity.Finite (Polynomial.X - Polynomial.C a) p
              def Polynomial.rootMultiplicity {R : Type u} [CommRing R] (a : R) (p : Polynomial R) :

              The largest power of X - C a which divides p. This is computable via the divisibility algorithm Polynomial.decidableDvdMonic.

              Equations
              Instances For
                theorem Polynomial.rootMultiplicity_eq_nat_find_of_nonzero {R : Type u} [CommRing R] {p : Polynomial R} (p0 : p 0) {a : R} :
                Polynomial.rootMultiplicity a p = Nat.find (_ : multiplicity.Finite (Polynomial.X - Polynomial.C a) p)
                theorem Polynomial.rootMultiplicity_eq_multiplicity {R : Type u} [CommRing R] (p : Polynomial R) (a : R) :
                Polynomial.rootMultiplicity a p = if h0 : p = 0 then 0 else Part.get (multiplicity (Polynomial.X - Polynomial.C a) p) (_ : multiplicity.Finite (Polynomial.X - Polynomial.C a) p)
                @[simp]
                theorem Polynomial.rootMultiplicity_C {R : Type u} [CommRing R] (r : R) (a : R) :
                Polynomial.rootMultiplicity a (Polynomial.C r) = 0
                theorem Polynomial.pow_rootMultiplicity_dvd {R : Type u} [CommRing R] (p : Polynomial R) (a : R) :
                (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p p
                theorem Polynomial.divByMonic_mul_pow_rootMultiplicity_eq {R : Type u} [CommRing R] (p : Polynomial R) (a : R) :
                p /ₘ (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p * (Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p = p
                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