Documentation

Mathlib.Algebra.Polynomial.Basic

Theory of univariate polynomials #

This file defines Polynomial R, the type of univariate polynomials over the semiring R, builds a semiring structure on it, and gives basic definitions that are expanded in other files in this directory.

Main definitions #

There are often two natural variants of lemmas involving sums, depending on whether one acts on the polynomials, or on the function. The naming convention is that one adds index when acting on the polynomials. For instance,

Implementation #

Polynomials are defined using R[ℕ], where R is a semiring. The variable X commutes with every polynomial p: lemma X_mul proves the identity X * p = p * X. The relationship to R[ℕ] is through a structure to make polynomials irreducible from the point of view of the kernel. Most operations are irreducible since Lean can not compute anyway with AddMonoidAlgebra. There are two exceptions that we make semireducible:

The raw implementation of the equivalence between R[X] and R[ℕ] is done through ofFinsupp and toFinsupp (or, equivalently, rcases p when p is a polynomial gives an element q of R[ℕ], and conversely ⟨q⟩ gives back p). The equivalence is also registered as a ring equiv in Polynomial.toFinsuppIso. These should in general not be used once the basic API for polynomials is constructed.

structure Polynomial (R : Type u_1) [Semiring R] :
Type u_1

Polynomial R is the type of univariate polynomials over R.

Polynomials should be seen as (semi-)rings with the additional constructor X. The embedding from R is called C.

Instances For

    Polynomial R is the type of univariate polynomials over R.

    Polynomials should be seen as (semi-)rings with the additional constructor X. The embedding from R is called C.

    Equations
    Instances For
      theorem Polynomial.forall_iff_forall_finsupp {R : Type u} [Semiring R] (P : Polynomial RProp) :
      (∀ (p : Polynomial R), P p) ∀ (q : AddMonoidAlgebra R ), P { toFinsupp := q }
      theorem Polynomial.exists_iff_exists_finsupp {R : Type u} [Semiring R] (P : Polynomial RProp) :
      (∃ (p : Polynomial R), P p) ∃ (q : AddMonoidAlgebra R ), P { toFinsupp := q }
      @[simp]
      theorem Polynomial.eta {R : Type u} [Semiring R] (f : Polynomial R) :
      { toFinsupp := f.toFinsupp } = f

      Conversions to and from AddMonoidAlgebra #

      Since R[X] is not defeq to R[ℕ], but instead is a structure wrapping it, we have to copy across all the arithmetic operators manually, along with the lemmas about how they unfold around Polynomial.ofFinsupp and Polynomial.toFinsupp.

      instance Polynomial.zero {R : Type u} [Semiring R] :
      Equations
      • Polynomial.zero = { zero := { toFinsupp := 0 } }
      instance Polynomial.one {R : Type u} [Semiring R] :
      Equations
      • Polynomial.one = { one := { toFinsupp := 1 } }
      instance Polynomial.add' {R : Type u} [Semiring R] :
      Equations
      • Polynomial.add' = { add := Polynomial.add }
      instance Polynomial.neg' {R : Type u} [Ring R] :
      Equations
      • Polynomial.neg' = { neg := Polynomial.neg }
      instance Polynomial.sub {R : Type u} [Ring R] :
      Equations
      instance Polynomial.mul' {R : Type u} [Semiring R] :
      Equations
      • Polynomial.mul' = { mul := Polynomial.mul }
      @[simp]
      theorem Polynomial.add_eq_add {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
      @[simp]
      theorem Polynomial.mul_eq_mul {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
      Equations
      @[instance 1]
      instance Polynomial.pow {R : Type u} [Semiring R] :
      Equations
      @[simp]
      theorem Polynomial.ofFinsupp_zero {R : Type u} [Semiring R] :
      { toFinsupp := 0 } = 0
      @[simp]
      theorem Polynomial.ofFinsupp_one {R : Type u} [Semiring R] :
      { toFinsupp := 1 } = 1
      @[simp]
      theorem Polynomial.ofFinsupp_add {R : Type u} [Semiring R] {a : AddMonoidAlgebra R } {b : AddMonoidAlgebra R } :
      { toFinsupp := a + b } = { toFinsupp := a } + { toFinsupp := b }
      @[simp]
      theorem Polynomial.ofFinsupp_neg {R : Type u} [Ring R] {a : AddMonoidAlgebra R } :
      { toFinsupp := -a } = -{ toFinsupp := a }
      @[simp]
      theorem Polynomial.ofFinsupp_sub {R : Type u} [Ring R] {a : AddMonoidAlgebra R } {b : AddMonoidAlgebra R } :
      { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
      @[simp]
      theorem Polynomial.ofFinsupp_mul {R : Type u} [Semiring R] (a : AddMonoidAlgebra R ) (b : AddMonoidAlgebra R ) :
      { toFinsupp := a * b } = { toFinsupp := a } * { toFinsupp := b }
      @[simp]
      theorem Polynomial.ofFinsupp_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (b : AddMonoidAlgebra R ) :
      { toFinsupp := a b } = a { toFinsupp := b }
      @[simp]
      theorem Polynomial.ofFinsupp_pow {R : Type u} [Semiring R] (a : AddMonoidAlgebra R ) (n : ) :
      { toFinsupp := a ^ n } = { toFinsupp := a } ^ n
      @[simp]
      theorem Polynomial.toFinsupp_add {R : Type u} [Semiring R] (a : Polynomial R) (b : Polynomial R) :
      (a + b).toFinsupp = a.toFinsupp + b.toFinsupp
      @[simp]
      theorem Polynomial.toFinsupp_neg {R : Type u} [Ring R] (a : Polynomial R) :
      (-a).toFinsupp = -a.toFinsupp
      @[simp]
      theorem Polynomial.toFinsupp_sub {R : Type u} [Ring R] (a : Polynomial R) (b : Polynomial R) :
      (a - b).toFinsupp = a.toFinsupp - b.toFinsupp
      @[simp]
      theorem Polynomial.toFinsupp_mul {R : Type u} [Semiring R] (a : Polynomial R) (b : Polynomial R) :
      (a * b).toFinsupp = a.toFinsupp * b.toFinsupp
      @[simp]
      theorem Polynomial.toFinsupp_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (b : Polynomial R) :
      (a b).toFinsupp = a b.toFinsupp
      @[simp]
      theorem Polynomial.toFinsupp_pow {R : Type u} [Semiring R] (a : Polynomial R) (n : ) :
      (a ^ n).toFinsupp = a.toFinsupp ^ n
      theorem IsSMulRegular.polynomial {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] {a : S} (ha : IsSMulRegular R a) :
      theorem Polynomial.toFinsupp_injective {R : Type u} [Semiring R] :
      Function.Injective Polynomial.toFinsupp
      @[simp]
      theorem Polynomial.toFinsupp_inj {R : Type u} [Semiring R] {a : Polynomial R} {b : Polynomial R} :
      a.toFinsupp = b.toFinsupp a = b
      @[simp]
      theorem Polynomial.toFinsupp_eq_zero {R : Type u} [Semiring R] {a : Polynomial R} :
      a.toFinsupp = 0 a = 0
      @[simp]
      theorem Polynomial.toFinsupp_eq_one {R : Type u} [Semiring R] {a : Polynomial R} :
      a.toFinsupp = 1 a = 1
      theorem Polynomial.ofFinsupp_inj {R : Type u} [Semiring R] {a : AddMonoidAlgebra R } {b : AddMonoidAlgebra R } :
      { toFinsupp := a } = { toFinsupp := b } a = b

      A more convenient spelling of Polynomial.ofFinsupp.injEq in terms of Iff.

      @[simp]
      theorem Polynomial.ofFinsupp_eq_zero {R : Type u} [Semiring R] {a : AddMonoidAlgebra R } :
      { toFinsupp := a } = 0 a = 0
      @[simp]
      theorem Polynomial.ofFinsupp_eq_one {R : Type u} [Semiring R] {a : AddMonoidAlgebra R } :
      { toFinsupp := a } = 1 a = 1
      Equations
      • Polynomial.inhabited = { default := 0 }
      Equations
      • Polynomial.instNatCast = { natCast := fun (n : ) => { toFinsupp := n } }
      Equations
      instance Polynomial.distribSMul {R : Type u} [Semiring R] {S : Type u_1} [DistribSMul S R] :
      Equations
      Equations
      Equations
      • =
      instance Polynomial.module {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] [Module S R] :
      Equations
      instance Polynomial.smulCommClass {R : Type u} [Semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R] :
      Equations
      • =
      instance Polynomial.isScalarTower {R : Type u} [Semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [IsScalarTower S₁ S₂ R] :
      Equations
      • =
      instance Polynomial.isScalarTower_right {α : Type u_1} {K : Type u_2} [Semiring K] [DistribSMul α K] [IsScalarTower α K K] :
      Equations
      • =
      Equations
      • Polynomial.unique = let __src := Polynomial.inhabited; { toInhabited := __src, uniq := }
      @[simp]
      theorem Polynomial.toFinsuppIso_symm_apply (R : Type u) [Semiring R] (toFinsupp : AddMonoidAlgebra R ) :
      (Polynomial.toFinsuppIso R).symm toFinsupp = { toFinsupp := toFinsupp }
      @[simp]
      theorem Polynomial.toFinsuppIso_apply (R : Type u) [Semiring R] (self : Polynomial R) :
      (Polynomial.toFinsuppIso R) self = self.toFinsupp

      Ring isomorphism between R[X] and R[ℕ]. This is just an implementation detail, but it can be useful to transfer results from Finsupp to polynomials.

      Equations
      • Polynomial.toFinsuppIso R = { toFun := Polynomial.toFinsupp, invFun := Polynomial.ofFinsupp, left_inv := , right_inv := , map_mul' := , map_add' := }
      Instances For
        theorem Polynomial.ofFinsupp_sum {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ιAddMonoidAlgebra R ) :
        { toFinsupp := is, f i } = is, { toFinsupp := f i }
        theorem Polynomial.toFinsupp_sum {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ιPolynomial R) :
        (is, f i).toFinsupp = is, (f i).toFinsupp

        The set of all n such that X^n has a non-zero coefficient.

        Equations
        • x.support = match x with | { toFinsupp := p } => p.support
        Instances For
          @[simp]
          theorem Polynomial.support_ofFinsupp {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ) :
          { toFinsupp := p }.support = p.support
          theorem Polynomial.support_toFinsupp {R : Type u} [Semiring R] (p : Polynomial R) :
          p.toFinsupp.support = p.support
          @[simp]
          theorem Polynomial.support_eq_empty {R : Type u} [Semiring R] {p : Polynomial R} :
          p.support = p = 0
          @[simp]
          theorem Polynomial.support_nonempty {R : Type u} [Semiring R] {p : Polynomial R} :
          p.support.Nonempty p 0
          theorem Polynomial.card_support_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} :
          p.support.card = 0 p = 0

          monomial s a is the monomial a * X^s

          Equations
          Instances For
            @[simp]
            theorem Polynomial.toFinsupp_monomial {R : Type u} [Semiring R] (n : ) (r : R) :
            ((Polynomial.monomial n) r).toFinsupp = Finsupp.single n r
            @[simp]
            theorem Polynomial.ofFinsupp_single {R : Type u} [Semiring R] (n : ) (r : R) :
            { toFinsupp := Finsupp.single n r } = (Polynomial.monomial n) r
            theorem Polynomial.monomial_add {R : Type u} [Semiring R] (n : ) (r : R) (s : R) :
            theorem Polynomial.monomial_mul_monomial {R : Type u} [Semiring R] (n : ) (m : ) (r : R) (s : R) :
            @[simp]
            theorem Polynomial.monomial_pow {R : Type u} [Semiring R] (n : ) (r : R) (k : ) :
            theorem Polynomial.smul_monomial {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (n : ) (b : R) :
            @[simp]
            theorem Polynomial.monomial_eq_zero_iff {R : Type u} [Semiring R] (t : R) (n : ) :
            theorem Polynomial.support_add {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
            (p + q).support p.support q.support

            C a is the constant polynomial a. C is provided as a ring homomorphism.

            Equations
            • Polynomial.C = let __src := Polynomial.monomial 0; { toFun := __src.toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
            Instances For
              @[simp]
              theorem Polynomial.monomial_zero_left {R : Type u} [Semiring R] (a : R) :
              (Polynomial.monomial 0) a = Polynomial.C a
              @[simp]
              theorem Polynomial.toFinsupp_C {R : Type u} [Semiring R] (a : R) :
              (Polynomial.C a).toFinsupp = AddMonoidAlgebra.single 0 a
              theorem Polynomial.C_0 {R : Type u} [Semiring R] :
              Polynomial.C 0 = 0
              theorem Polynomial.C_1 {R : Type u} [Semiring R] :
              Polynomial.C 1 = 1
              theorem Polynomial.C_mul {R : Type u} {a : R} {b : R} [Semiring R] :
              Polynomial.C (a * b) = Polynomial.C a * Polynomial.C b
              theorem Polynomial.C_add {R : Type u} {a : R} {b : R} [Semiring R] :
              Polynomial.C (a + b) = Polynomial.C a + Polynomial.C b
              @[simp]
              theorem Polynomial.smul_C {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (s : S) (r : R) :
              s Polynomial.C r = Polynomial.C (s r)
              theorem Polynomial.C_pow {R : Type u} {a : R} {n : } [Semiring R] :
              Polynomial.C (a ^ n) = Polynomial.C a ^ n
              theorem Polynomial.C_eq_natCast {R : Type u} [Semiring R] (n : ) :
              Polynomial.C n = n
              @[deprecated Polynomial.C_eq_natCast]
              theorem Polynomial.C_eq_nat_cast {R : Type u} [Semiring R] (n : ) :
              Polynomial.C n = n

              Alias of Polynomial.C_eq_natCast.

              @[simp]
              theorem Polynomial.C_mul_monomial {R : Type u} {a : R} {b : R} {n : } [Semiring R] :
              Polynomial.C a * (Polynomial.monomial n) b = (Polynomial.monomial n) (a * b)
              @[simp]
              theorem Polynomial.monomial_mul_C {R : Type u} {a : R} {b : R} {n : } [Semiring R] :
              (Polynomial.monomial n) a * Polynomial.C b = (Polynomial.monomial n) (a * b)

              X is the polynomial variable (aka indeterminate).

              Equations
              Instances For
                theorem Polynomial.monomial_one_right_eq_X_pow {R : Type u} [Semiring R] (n : ) :
                (Polynomial.monomial n) 1 = Polynomial.X ^ n
                @[simp]
                theorem Polynomial.toFinsupp_X {R : Type u} [Semiring R] :
                Polynomial.X.toFinsupp = Finsupp.single 1 1
                theorem Polynomial.X_mul {R : Type u} [Semiring R] {p : Polynomial R} :
                Polynomial.X * p = p * Polynomial.X

                X commutes with everything, even when the coefficients are noncommutative.

                theorem Polynomial.X_pow_mul {R : Type u} [Semiring R] {p : Polynomial R} {n : } :
                Polynomial.X ^ n * p = p * Polynomial.X ^ n
                @[simp]
                theorem Polynomial.X_mul_C {R : Type u} [Semiring R] (r : R) :
                Polynomial.X * Polynomial.C r = Polynomial.C r * Polynomial.X

                Prefer putting constants to the left of X.

                This lemma is the loop-avoiding simp version of Polynomial.X_mul.

                @[simp]
                theorem Polynomial.X_pow_mul_C {R : Type u} [Semiring R] (r : R) (n : ) :
                Polynomial.X ^ n * Polynomial.C r = Polynomial.C r * Polynomial.X ^ n

                Prefer putting constants to the left of X ^ n.

                This lemma is the loop-avoiding simp version of X_pow_mul.

                theorem Polynomial.X_pow_mul_assoc {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} {n : } :
                p * Polynomial.X ^ n * q = p * q * Polynomial.X ^ n
                @[simp]
                theorem Polynomial.X_pow_mul_assoc_C {R : Type u} [Semiring R] {p : Polynomial R} {n : } (r : R) :
                p * Polynomial.X ^ n * Polynomial.C r = p * Polynomial.C r * Polynomial.X ^ n

                Prefer putting constants to the left of X ^ n.

                This lemma is the loop-avoiding simp version of X_pow_mul_assoc.

                theorem Polynomial.commute_X {R : Type u} [Semiring R] (p : Polynomial R) :
                Commute Polynomial.X p
                theorem Polynomial.commute_X_pow {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
                Commute (Polynomial.X ^ n) p
                @[simp]
                theorem Polynomial.monomial_mul_X {R : Type u} [Semiring R] (n : ) (r : R) :
                (Polynomial.monomial n) r * Polynomial.X = (Polynomial.monomial (n + 1)) r
                @[simp]
                theorem Polynomial.monomial_mul_X_pow {R : Type u} [Semiring R] (n : ) (r : R) (k : ) :
                (Polynomial.monomial n) r * Polynomial.X ^ k = (Polynomial.monomial (n + k)) r
                @[simp]
                theorem Polynomial.X_mul_monomial {R : Type u} [Semiring R] (n : ) (r : R) :
                Polynomial.X * (Polynomial.monomial n) r = (Polynomial.monomial (n + 1)) r
                @[simp]
                theorem Polynomial.X_pow_mul_monomial {R : Type u} [Semiring R] (k : ) (n : ) (r : R) :
                Polynomial.X ^ k * (Polynomial.monomial n) r = (Polynomial.monomial (n + k)) r
                def Polynomial.coeff {R : Type u} [Semiring R] :
                Polynomial RR

                coeff p n (often denoted p.coeff n) is the coefficient of X^n in p.

                Equations
                • x.coeff = match (motive := Polynomial RR) x with | { toFinsupp := p } => p
                Instances For
                  @[simp]
                  theorem Polynomial.coeff_ofFinsupp {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ) :
                  { toFinsupp := p }.coeff = p
                  @[simp]
                  theorem Polynomial.coeff_inj {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
                  p.coeff = q.coeff p = q
                  theorem Polynomial.toFinsupp_apply {R : Type u} [Semiring R] (f : Polynomial R) (i : ) :
                  f.toFinsupp i = f.coeff i
                  theorem Polynomial.coeff_monomial {R : Type u} {a : R} {m : } {n : } [Semiring R] :
                  ((Polynomial.monomial n) a).coeff m = if n = m then a else 0
                  @[simp]
                  theorem Polynomial.coeff_zero {R : Type u} [Semiring R] (n : ) :
                  theorem Polynomial.coeff_one {R : Type u} [Semiring R] {n : } :
                  Polynomial.coeff 1 n = if n = 0 then 1 else 0
                  @[simp]
                  theorem Polynomial.coeff_X_one {R : Type u} [Semiring R] :
                  Polynomial.X.coeff 1 = 1
                  @[simp]
                  theorem Polynomial.coeff_X_zero {R : Type u} [Semiring R] :
                  Polynomial.X.coeff 0 = 0
                  @[simp]
                  theorem Polynomial.coeff_monomial_succ {R : Type u} {a : R} {n : } [Semiring R] :
                  ((Polynomial.monomial (n + 1)) a).coeff 0 = 0
                  theorem Polynomial.coeff_X {R : Type u} {n : } [Semiring R] :
                  Polynomial.X.coeff n = if 1 = n then 1 else 0
                  theorem Polynomial.coeff_X_of_ne_one {R : Type u} [Semiring R] {n : } (hn : n 1) :
                  Polynomial.X.coeff n = 0
                  @[simp]
                  theorem Polynomial.mem_support_iff {R : Type u} {n : } [Semiring R] {p : Polynomial R} :
                  n p.support p.coeff n 0
                  theorem Polynomial.not_mem_support_iff {R : Type u} {n : } [Semiring R] {p : Polynomial R} :
                  np.support p.coeff n = 0
                  theorem Polynomial.coeff_C {R : Type u} {a : R} {n : } [Semiring R] :
                  (Polynomial.C a).coeff n = if n = 0 then a else 0
                  @[simp]
                  theorem Polynomial.coeff_C_zero {R : Type u} {a : R} [Semiring R] :
                  (Polynomial.C a).coeff 0 = a
                  theorem Polynomial.coeff_C_ne_zero {R : Type u} {a : R} {n : } [Semiring R] (h : n 0) :
                  (Polynomial.C a).coeff n = 0
                  @[simp]
                  theorem Polynomial.coeff_C_succ {R : Type u} [Semiring R] {r : R} {n : } :
                  (Polynomial.C r).coeff (n + 1) = 0
                  @[simp]
                  theorem Polynomial.coeff_natCast_ite {R : Type u} {m : } {n : } [Semiring R] :
                  (m).coeff n = (if n = 0 then m else 0)
                  @[deprecated Polynomial.coeff_natCast_ite]
                  theorem Polynomial.coeff_nat_cast_ite {R : Type u} {m : } {n : } [Semiring R] :
                  (m).coeff n = (if n = 0 then m else 0)

                  Alias of Polynomial.coeff_natCast_ite.

                  @[simp]
                  theorem Polynomial.coeff_ofNat_zero {R : Type u} [Semiring R] (a : ) [a.AtLeastTwo] :
                  (OfNat.ofNat a).coeff 0 = OfNat.ofNat a
                  @[simp]
                  theorem Polynomial.coeff_ofNat_succ {R : Type u} [Semiring R] (a : ) (n : ) [h : a.AtLeastTwo] :
                  (OfNat.ofNat a).coeff (n + 1) = 0
                  theorem Polynomial.C_mul_X_pow_eq_monomial {R : Type u} {a : R} [Semiring R] {n : } :
                  Polynomial.C a * Polynomial.X ^ n = (Polynomial.monomial n) a
                  @[simp]
                  theorem Polynomial.toFinsupp_C_mul_X_pow {R : Type u} [Semiring R] (a : R) (n : ) :
                  (Polynomial.C a * Polynomial.X ^ n).toFinsupp = Finsupp.single n a
                  theorem Polynomial.C_mul_X_eq_monomial {R : Type u} {a : R} [Semiring R] :
                  Polynomial.C a * Polynomial.X = (Polynomial.monomial 1) a
                  @[simp]
                  theorem Polynomial.toFinsupp_C_mul_X {R : Type u} [Semiring R] (a : R) :
                  (Polynomial.C a * Polynomial.X).toFinsupp = Finsupp.single 1 a
                  theorem Polynomial.C_injective {R : Type u} [Semiring R] :
                  Function.Injective Polynomial.C
                  @[simp]
                  theorem Polynomial.C_inj {R : Type u} {a : R} {b : R} [Semiring R] :
                  Polynomial.C a = Polynomial.C b a = b
                  @[simp]
                  theorem Polynomial.C_eq_zero {R : Type u} {a : R} [Semiring R] :
                  Polynomial.C a = 0 a = 0
                  theorem Polynomial.C_ne_zero {R : Type u} {a : R} [Semiring R] :
                  Polynomial.C a 0 a 0
                  theorem Polynomial.forall_eq_iff_forall_eq {R : Type u} [Semiring R] :
                  (∀ (f g : Polynomial R), f = g) ∀ (a b : R), a = b
                  theorem Polynomial.ext_iff {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
                  p = q ∀ (n : ), p.coeff n = q.coeff n
                  theorem Polynomial.ext {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
                  (∀ (n : ), p.coeff n = q.coeff n)p = q

                  Monomials generate the additive monoid of polynomials.

                  theorem Polynomial.addHom_ext {R : Type u} [Semiring R] {M : Type u_1} [AddMonoid M] {f : Polynomial R →+ M} {g : Polynomial R →+ M} (h : ∀ (n : ) (a : R), f ((Polynomial.monomial n) a) = g ((Polynomial.monomial n) a)) :
                  f = g
                  theorem Polynomial.addHom_ext' {R : Type u} [Semiring R] {M : Type u_1} [AddMonoid M] {f : Polynomial R →+ M} {g : Polynomial R →+ M} (h : ∀ (n : ), f.comp (Polynomial.monomial n).toAddMonoidHom = g.comp (Polynomial.monomial n).toAddMonoidHom) :
                  f = g
                  theorem Polynomial.lhom_ext' {R : Type u} [Semiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {f : Polynomial R →ₗ[R] M} {g : Polynomial R →ₗ[R] M} (h : ∀ (n : ), f ∘ₗ Polynomial.monomial n = g ∘ₗ Polynomial.monomial n) :
                  f = g
                  theorem Polynomial.eq_zero_of_eq_zero {R : Type u} [Semiring R] (h : 0 = 1) (p : Polynomial R) :
                  p = 0
                  theorem Polynomial.support_monomial {R : Type u} [Semiring R] (n : ) {a : R} (H : a 0) :
                  ((Polynomial.monomial n) a).support = {n}
                  theorem Polynomial.support_monomial' {R : Type u} [Semiring R] (n : ) (a : R) :
                  ((Polynomial.monomial n) a).support {n}
                  theorem Polynomial.support_C_mul_X {R : Type u} [Semiring R] {c : R} (h : c 0) :
                  (Polynomial.C c * Polynomial.X).support = {1}
                  theorem Polynomial.support_C_mul_X' {R : Type u} [Semiring R] (c : R) :
                  (Polynomial.C c * Polynomial.X).support {1}
                  theorem Polynomial.support_C_mul_X_pow {R : Type u} [Semiring R] (n : ) {c : R} (h : c 0) :
                  (Polynomial.C c * Polynomial.X ^ n).support = {n}
                  theorem Polynomial.support_C_mul_X_pow' {R : Type u} [Semiring R] (n : ) (c : R) :
                  (Polynomial.C c * Polynomial.X ^ n).support {n}
                  theorem Polynomial.support_binomial' {R : Type u} [Semiring R] (k : ) (m : ) (x : R) (y : R) :
                  (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support {k, m}
                  theorem Polynomial.support_trinomial' {R : Type u} [Semiring R] (k : ) (m : ) (n : ) (x : R) (y : R) (z : R) :
                  (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support {k, m, n}
                  theorem Polynomial.X_pow_eq_monomial {R : Type u} [Semiring R] (n : ) :
                  Polynomial.X ^ n = (Polynomial.monomial n) 1
                  @[simp]
                  theorem Polynomial.toFinsupp_X_pow {R : Type u} [Semiring R] (n : ) :
                  (Polynomial.X ^ n).toFinsupp = Finsupp.single n 1
                  theorem Polynomial.smul_X_eq_monomial {R : Type u} {a : R} [Semiring R] {n : } :
                  a Polynomial.X ^ n = (Polynomial.monomial n) a
                  theorem Polynomial.support_X_pow {R : Type u} [Semiring R] (H : ¬1 = 0) (n : ) :
                  (Polynomial.X ^ n).support = {n}
                  theorem Polynomial.support_X_empty {R : Type u} [Semiring R] (H : 1 = 0) :
                  Polynomial.X.support =
                  theorem Polynomial.support_X {R : Type u} [Semiring R] (H : ¬1 = 0) :
                  Polynomial.X.support = {1}
                  theorem Polynomial.monomial_left_inj {R : Type u} [Semiring R] {a : R} (ha : a 0) {i : } {j : } :
                  theorem Polynomial.binomial_eq_binomial {R : Type u} [Semiring R] {k : } {l : } {m : } {n : } {u : R} {v : R} (hu : u 0) (hv : v 0) :
                  Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ l = Polynomial.C u * Polynomial.X ^ m + Polynomial.C v * Polynomial.X ^ n k = m l = n u = v k = n l = m u + v = 0 k = l m = n
                  theorem Polynomial.natCast_mul {R : Type u} [Semiring R] (n : ) (p : Polynomial R) :
                  n * p = n p
                  @[deprecated Polynomial.natCast_mul]
                  theorem Polynomial.nat_cast_mul {R : Type u} [Semiring R] (n : ) (p : Polynomial R) :
                  n * p = n p

                  Alias of Polynomial.natCast_mul.

                  def Polynomial.sum {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : RS) :
                  S

                  Summing the values of a function applied to the coefficients of a polynomial

                  Equations
                  • p.sum f = np.support, f n (p.coeff n)
                  Instances For
                    theorem Polynomial.sum_def {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : RS) :
                    p.sum f = np.support, f n (p.coeff n)
                    theorem Polynomial.sum_eq_of_subset {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {p : Polynomial R} (f : RS) (hf : ∀ (i : ), f i 0 = 0) {s : Finset } (hs : p.support s) :
                    p.sum f = ns, f n (p.coeff n)
                    theorem Polynomial.mul_eq_sum_sum {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
                    p * q = ip.support, q.sum fun (j : ) (a : R) => (Polynomial.monomial (i + j)) (p.coeff i * a)

                    Expressing the product of two polynomials as a double sum.

                    @[simp]
                    theorem Polynomial.sum_zero_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (f : RS) :
                    @[simp]
                    theorem Polynomial.sum_monomial_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {n : } (a : R) (f : RS) (hf : f n 0 = 0) :
                    ((Polynomial.monomial n) a).sum f = f n a
                    @[simp]
                    theorem Polynomial.sum_C_index {R : Type u} [Semiring R] {a : R} {β : Type u_1} [AddCommMonoid β] {f : Rβ} (h : f 0 0 = 0) :
                    (Polynomial.C a).sum f = f 0 a
                    @[simp]
                    theorem Polynomial.sum_X_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {f : RS} (hf : f 1 0 = 0) :
                    Polynomial.X.sum f = f 1 1
                    theorem Polynomial.sum_add_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (q : Polynomial R) (f : RS) (hf : ∀ (i : ), f i 0 = 0) (h_add : ∀ (a : ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂) :
                    (p + q).sum f = p.sum f + q.sum f
                    theorem Polynomial.sum_add' {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : RS) (g : RS) :
                    p.sum (f + g) = p.sum f + p.sum g
                    theorem Polynomial.sum_add {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : RS) (g : RS) :
                    (p.sum fun (n : ) (x : R) => f n x + g n x) = p.sum f + p.sum g
                    theorem Polynomial.sum_smul_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (b : R) (f : RS) (hf : ∀ (i : ), f i 0 = 0) :
                    (b p).sum f = p.sum fun (n : ) (a : R) => f n (b * a)
                    @[simp]
                    theorem Polynomial.sum_monomial_eq {R : Type u} [Semiring R] (p : Polynomial R) :
                    (p.sum fun (n : ) (a : R) => (Polynomial.monomial n) a) = p
                    theorem Polynomial.sum_C_mul_X_pow_eq {R : Type u} [Semiring R] (p : Polynomial R) :
                    (p.sum fun (n : ) (a : R) => Polynomial.C a * Polynomial.X ^ n) = p
                    @[irreducible]
                    def Polynomial.erase {R : Type u_1} [Semiring R] (n : ) :

                    erase p n is the polynomial p in which the X^n term has been erased.

                    Equations
                    Instances For
                      theorem Polynomial.erase_def {R : Type u_1} [Semiring R] (n : ) :
                      ∀ (x : Polynomial R), Polynomial.erase n x = match x with | { toFinsupp := p } => { toFinsupp := Finsupp.erase n p }
                      @[simp]
                      theorem Polynomial.toFinsupp_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
                      (Polynomial.erase n p).toFinsupp = Finsupp.erase n p.toFinsupp
                      @[simp]
                      theorem Polynomial.ofFinsupp_erase {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ) (n : ) :
                      { toFinsupp := Finsupp.erase n p } = Polynomial.erase n { toFinsupp := p }
                      @[simp]
                      theorem Polynomial.support_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
                      (Polynomial.erase n p).support = p.support.erase n
                      theorem Polynomial.monomial_add_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
                      (Polynomial.monomial n) (p.coeff n) + Polynomial.erase n p = p
                      theorem Polynomial.coeff_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (i : ) :
                      (Polynomial.erase n p).coeff i = if i = n then 0 else p.coeff i
                      @[simp]
                      theorem Polynomial.erase_zero {R : Type u} [Semiring R] (n : ) :
                      @[simp]
                      theorem Polynomial.erase_monomial {R : Type u} [Semiring R] {n : } {a : R} :
                      @[simp]
                      theorem Polynomial.erase_same {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
                      (Polynomial.erase n p).coeff n = 0
                      @[simp]
                      theorem Polynomial.erase_ne {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (i : ) (h : i n) :
                      (Polynomial.erase n p).coeff i = p.coeff i
                      def Polynomial.update {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (a : R) :

                      Replace the coefficient of a p : R[X] at a given degree n : ℕ by a given value a : R. If a = 0, this is equal to p.erase n If p.natDegree < n and a ≠ 0, this increases the degree to n.

                      Equations
                      Instances For
                        theorem Polynomial.coeff_update {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (a : R) :
                        (p.update n a).coeff = Function.update p.coeff n a
                        theorem Polynomial.coeff_update_apply {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (a : R) (i : ) :
                        (p.update n a).coeff i = if i = n then a else p.coeff i
                        @[simp]
                        theorem Polynomial.coeff_update_same {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (a : R) :
                        (p.update n a).coeff n = a
                        theorem Polynomial.coeff_update_ne {R : Type u} [Semiring R] (p : Polynomial R) {n : } (a : R) {i : } (h : i n) :
                        (p.update n a).coeff i = p.coeff i
                        @[simp]
                        theorem Polynomial.update_zero_eq_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
                        p.update n 0 = Polynomial.erase n p
                        theorem Polynomial.support_update {R : Type u} [Semiring R] (p : Polynomial R) (n : ) (a : R) [Decidable (a = 0)] :
                        (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
                        theorem Polynomial.support_update_zero {R : Type u} [Semiring R] (p : Polynomial R) (n : ) :
                        (p.update n 0).support = p.support.erase n
                        theorem Polynomial.support_update_ne_zero {R : Type u} [Semiring R] (p : Polynomial R) (n : ) {a : R} (ha : a 0) :
                        (p.update n a).support = insert n p.support
                        Equations
                        Equations
                        • Polynomial.instIntCast = { intCast := fun (n : ) => { toFinsupp := n } }
                        instance Polynomial.ring {R : Type u} [Ring R] :
                        Equations
                        @[simp]
                        theorem Polynomial.coeff_neg {R : Type u} [Ring R] (p : Polynomial R) (n : ) :
                        (-p).coeff n = -p.coeff n
                        @[simp]
                        theorem Polynomial.coeff_sub {R : Type u} [Ring R] (p : Polynomial R) (q : Polynomial R) (n : ) :
                        (p - q).coeff n = p.coeff n - q.coeff n
                        theorem Polynomial.monomial_neg {R : Type u} [Ring R] (n : ) (a : R) :
                        theorem Polynomial.monomial_sub {R : Type u} {a : R} {b : R} [Ring R] (n : ) :
                        @[simp]
                        theorem Polynomial.support_neg {R : Type u} [Ring R] {p : Polynomial R} :
                        (-p).support = p.support
                        theorem Polynomial.C_eq_intCast {R : Type u} [Ring R] (n : ) :
                        Polynomial.C n = n
                        @[deprecated Polynomial.C_eq_intCast]
                        theorem Polynomial.C_eq_int_cast {R : Type u} [Ring R] (n : ) :
                        Polynomial.C n = n

                        Alias of Polynomial.C_eq_intCast.

                        theorem Polynomial.C_neg {R : Type u} {a : R} [Ring R] :
                        Polynomial.C (-a) = -Polynomial.C a
                        theorem Polynomial.C_sub {R : Type u} {a : R} {b : R} [Ring R] :
                        Polynomial.C (a - b) = Polynomial.C a - Polynomial.C b
                        Equations
                        Equations
                        • =
                        @[simp]
                        theorem Polynomial.X_ne_zero {R : Type u} [Semiring R] [Nontrivial R] :
                        Polynomial.X 0
                        theorem Polynomial.nnqsmul_eq_C_mul {R : Type u} [DivisionSemiring R] (q : ℚ≥0) (f : Polynomial R) :
                        q f = Polynomial.C q * f
                        theorem Polynomial.qsmul_eq_C_mul {R : Type u} [DivisionRing R] (a : ) (f : Polynomial R) :
                        a f = Polynomial.C a * f
                        instance Polynomial.repr {R : Type u} [Semiring R] [Repr R] [DecidableEq R] :
                        Equations
                        • One or more equations did not get rendered due to their size.