Documentation

Mathlib.Data.MvPolynomial.Basic

Multivariate polynomials #

This file defines polynomial rings over a base ring (or even semiring), with variables from a general type σ (which could be infinite).

Important definitions #

Let R be a commutative ring (or a semiring) and let σ be an arbitrary type. This file creates the type MvPolynomial σ R, which mathematicians might denote $R[X_i : i \in σ]$. It is the type of multivariate (a.k.a. multivariable) polynomials, with variables corresponding to the terms in σ, and coefficients in R.

Notation #

In the definitions below, we use the following notation:

Definitions #

Implementation notes #

Recall that if Y has a zero, then X →₀ Y is the type of functions from X to Y with finite support, i.e. such that only finitely many elements of X get sent to non-zero terms in Y. The definition of MvPolynomial σ R is (σ →₀ ℕ) →₀ R; here σ →₀ ℕ denotes the space of all monomials in the variables, and the function to R sends a monomial to its coefficient in the polynomial being represented.

Tags #

polynomial, multivariate polynomial, multivariable polynomial

def MvPolynomial (σ : Type u_1) (R : Type u_2) [CommSemiring R] :
Type (max u_1 u_2)

Multivariate polynomial, where σ is the index set of the variables and R is the coefficient ring

Equations
Instances For
    Equations
    • MvPolynomial.decidableEqMvPolynomial = Finsupp.instDecidableEq
    Equations
    • MvPolynomial.commSemiring = AddMonoidAlgebra.commSemiring
    instance MvPolynomial.inhabited {R : Type u} {σ : Type u_1} [CommSemiring R] :
    Equations
    • MvPolynomial.inhabited = { default := 0 }
    instance MvPolynomial.distribuMulAction {R : Type u} {S₁ : Type v} {σ : Type u_1} [Monoid R] [CommSemiring S₁] [DistribMulAction R S₁] :
    Equations
    • MvPolynomial.distribuMulAction = AddMonoidAlgebra.distribMulAction
    instance MvPolynomial.smulZeroClass {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [SMulZeroClass R S₁] :
    Equations
    • MvPolynomial.smulZeroClass = AddMonoidAlgebra.smulZeroClass
    instance MvPolynomial.faithfulSMul {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [SMulZeroClass R S₁] [FaithfulSMul R S₁] :
    Equations
    • =
    instance MvPolynomial.module {R : Type u} {S₁ : Type v} {σ : Type u_1} [Semiring R] [CommSemiring S₁] [Module R S₁] :
    Module R (MvPolynomial σ S₁)
    Equations
    • MvPolynomial.module = AddMonoidAlgebra.module
    instance MvPolynomial.isScalarTower {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring S₂] [SMul R S₁] [SMulZeroClass R S₂] [SMulZeroClass S₁ S₂] [IsScalarTower R S₁ S₂] :
    IsScalarTower R S₁ (MvPolynomial σ S₂)
    Equations
    • =
    instance MvPolynomial.smulCommClass {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring S₂] [SMulZeroClass R S₂] [SMulZeroClass S₁ S₂] [SMulCommClass R S₁ S₂] :
    SMulCommClass R S₁ (MvPolynomial σ S₂)
    Equations
    • =
    instance MvPolynomial.isCentralScalar {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [SMulZeroClass R S₁] [SMulZeroClass Rᵐᵒᵖ S₁] [IsCentralScalar R S₁] :
    Equations
    • =
    instance MvPolynomial.algebra {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] :
    Algebra R (MvPolynomial σ S₁)
    Equations
    • MvPolynomial.algebra = AddMonoidAlgebra.algebra
    instance MvPolynomial.isScalarTower_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [DistribSMul R S₁] [IsScalarTower R S₁ S₁] :
    Equations
    • =
    instance MvPolynomial.smulCommClass_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [DistribSMul R S₁] [SMulCommClass R S₁ S₁] :
    Equations
    • =
    instance MvPolynomial.unique {R : Type u} {σ : Type u_1} [CommSemiring R] [Subsingleton R] :

    If R is a subsingleton, then MvPolynomial σ R has a unique element

    Equations
    • MvPolynomial.unique = AddMonoidAlgebra.unique
    def MvPolynomial.monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ) :

    monomial s a is the monomial with coefficient a and exponents given by s

    Equations
    Instances For
      theorem MvPolynomial.mul_def {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} :
      p * q = Finsupp.sum p fun (m : σ →₀ ) (a : R) => Finsupp.sum q fun (n : σ →₀ ) (b : R) => (MvPolynomial.monomial (m + n)) (a * b)
      def MvPolynomial.C {R : Type u} {σ : Type u_1} [CommSemiring R] :

      C a is the constant polynomial with value a

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem MvPolynomial.algebraMap_eq (R : Type u) (σ : Type u_1) [CommSemiring R] :
        algebraMap R (MvPolynomial σ R) = MvPolynomial.C
        def MvPolynomial.X {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) :

        X n is the degree 1 monomial $X_n$.

        Equations
        Instances For
          theorem MvPolynomial.monomial_left_injective {R : Type u} {σ : Type u_1} [CommSemiring R] {r : R} (hr : r 0) :
          @[simp]
          theorem MvPolynomial.monomial_left_inj {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ } {t : σ →₀ } {r : R} (hr : r 0) :
          theorem MvPolynomial.C_apply {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] :
          MvPolynomial.C a = (MvPolynomial.monomial 0) a
          theorem MvPolynomial.C_0 {R : Type u} {σ : Type u_1} [CommSemiring R] :
          MvPolynomial.C 0 = 0
          theorem MvPolynomial.C_1 {R : Type u} {σ : Type u_1} [CommSemiring R] :
          MvPolynomial.C 1 = 1
          theorem MvPolynomial.C_mul_monomial {R : Type u} {σ : Type u_1} {a : R} {a' : R} {s : σ →₀ } [CommSemiring R] :
          MvPolynomial.C a * (MvPolynomial.monomial s) a' = (MvPolynomial.monomial s) (a * a')
          theorem MvPolynomial.C_add {R : Type u} {σ : Type u_1} {a : R} {a' : R} [CommSemiring R] :
          MvPolynomial.C (a + a') = MvPolynomial.C a + MvPolynomial.C a'
          theorem MvPolynomial.C_mul {R : Type u} {σ : Type u_1} {a : R} {a' : R} [CommSemiring R] :
          MvPolynomial.C (a * a') = MvPolynomial.C a * MvPolynomial.C a'
          theorem MvPolynomial.C_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) (n : ) :
          MvPolynomial.C (a ^ n) = MvPolynomial.C a ^ n
          theorem MvPolynomial.C_injective (σ : Type u_2) (R : Type u_3) [CommSemiring R] :
          Function.Injective MvPolynomial.C
          theorem MvPolynomial.C_surjective {R : Type u_2} [CommSemiring R] (σ : Type u_3) [IsEmpty σ] :
          Function.Surjective MvPolynomial.C
          @[simp]
          theorem MvPolynomial.C_inj {σ : Type u_2} (R : Type u_3) [CommSemiring R] (r : R) (s : R) :
          MvPolynomial.C r = MvPolynomial.C s r = s
          Equations
          • =
          Equations
          • =
          Equations
          • =
          theorem MvPolynomial.C_eq_coe_nat {R : Type u} {σ : Type u_1} [CommSemiring R] (n : ) :
          MvPolynomial.C n = n
          theorem MvPolynomial.C_mul' {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] {p : MvPolynomial σ R} :
          MvPolynomial.C a * p = a p
          theorem MvPolynomial.smul_eq_C_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (a : R) :
          a p = MvPolynomial.C a * p
          theorem MvPolynomial.C_eq_smul_one {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] :
          MvPolynomial.C a = a 1
          theorem MvPolynomial.smul_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [CommSemiring R] {S₁ : Type u_2} [SMulZeroClass S₁ R] (r : S₁) :
          theorem MvPolynomial.X_injective {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] :
          Function.Injective MvPolynomial.X
          @[simp]
          theorem MvPolynomial.X_inj {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (m : σ) (n : σ) :
          theorem MvPolynomial.monomial_pow {R : Type u} {σ : Type u_1} {a : R} {e : } {s : σ →₀ } [CommSemiring R] :
          @[simp]
          theorem MvPolynomial.monomial_mul {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ } {s' : σ →₀ } {a : R} {b : R} :

          fun s ↦ monomial s 1 as a homomorphism.

          Equations
          Instances For
            theorem MvPolynomial.monomial_add_single {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ } [CommSemiring R] :
            theorem MvPolynomial.monomial_single_add {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ } [CommSemiring R] :
            theorem MvPolynomial.C_mul_X_pow_eq_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ} {a : R} {n : } :
            MvPolynomial.C a * MvPolynomial.X s ^ n = (MvPolynomial.monomial (Finsupp.single s n)) a
            theorem MvPolynomial.C_mul_X_eq_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ} {a : R} :
            theorem MvPolynomial.monomial_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ } :
            @[simp]
            theorem MvPolynomial.monomial_zero' {R : Type u} {σ : Type u_1} [CommSemiring R] :
            (MvPolynomial.monomial 0) = MvPolynomial.C
            @[simp]
            theorem MvPolynomial.monomial_eq_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ } {b : R} :
            @[simp]
            theorem MvPolynomial.sum_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] {u : σ →₀ } {r : R} {b : (σ →₀ )RA} (w : b u 0 = 0) :
            @[simp]
            theorem MvPolynomial.sum_C {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] {b : (σ →₀ )RA} (w : b 0 0 = 0) :
            Finsupp.sum (MvPolynomial.C a) b = b 0 a
            theorem MvPolynomial.monomial_sum_one {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} (s : Finset α) (f : ασ →₀ ) :
            (MvPolynomial.monomial (Finset.sum s fun (i : α) => f i)) 1 = Finset.prod s fun (i : α) => (MvPolynomial.monomial (f i)) 1
            theorem MvPolynomial.monomial_sum_index {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} (s : Finset α) (f : ασ →₀ ) (a : R) :
            (MvPolynomial.monomial (Finset.sum s fun (i : α) => f i)) a = MvPolynomial.C a * Finset.prod s fun (i : α) => (MvPolynomial.monomial (f i)) 1
            theorem MvPolynomial.monomial_finsupp_sum_index {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [Zero β] (f : α →₀ β) (g : αβσ →₀ ) (a : R) :
            (MvPolynomial.monomial (Finsupp.sum f g)) a = MvPolynomial.C a * Finsupp.prod f fun (a : α) (b : β) => (MvPolynomial.monomial (g a b)) 1
            theorem MvPolynomial.monomial_eq_monomial_iff {R : Type u} [CommSemiring R] {α : Type u_2} (a₁ : α →₀ ) (a₂ : α →₀ ) (b₁ : R) (b₂ : R) :
            (MvPolynomial.monomial a₁) b₁ = (MvPolynomial.monomial a₂) b₂ a₁ = a₂ b₁ = b₂ b₁ = 0 b₂ = 0
            theorem MvPolynomial.monomial_eq {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [CommSemiring R] :
            (MvPolynomial.monomial s) a = MvPolynomial.C a * Finsupp.prod s fun (n : σ) (e : ) => MvPolynomial.X n ^ e
            @[simp]
            theorem MvPolynomial.prod_X_pow_eq_monomial {R : Type u} {σ : Type u_1} {s : σ →₀ } [CommSemiring R] :
            (Finset.prod s.support fun (x : σ) => MvPolynomial.X x ^ s x) = (MvPolynomial.monomial s) 1
            theorem MvPolynomial.induction_on_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] {M : MvPolynomial σ RProp} (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_X : ∀ (p : MvPolynomial σ R) (n : σ), M pM (p * MvPolynomial.X n)) (s : σ →₀ ) (a : R) :
            theorem MvPolynomial.induction_on' {R : Type u} {σ : Type u_1} [CommSemiring R] {P : MvPolynomial σ RProp} (p : MvPolynomial σ R) (h1 : ∀ (u : σ →₀ ) (a : R), P ((MvPolynomial.monomial u) a)) (h2 : ∀ (p q : MvPolynomial σ R), P pP qP (p + q)) :
            P p

            Analog of Polynomial.induction_on'. To prove something about mv_polynomials, it suffices to show the condition is closed under taking sums, and it holds for monomials.

            theorem MvPolynomial.induction_on''' {R : Type u} {σ : Type u_1} [CommSemiring R] {M : MvPolynomial σ RProp} (p : MvPolynomial σ R) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add_weak : ∀ (a : σ →₀ ) (b : R) (f : (σ →₀ ) →₀ R), af.supportb 0M fM ((let_fun this := (MvPolynomial.monomial a) b; this) + f)) :
            M p

            Similar to MvPolynomial.induction_on but only a weak form of h_add is required.

            theorem MvPolynomial.induction_on'' {R : Type u} {σ : Type u_1} [CommSemiring R] {M : MvPolynomial σ RProp} (p : MvPolynomial σ R) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add_weak : ∀ (a : σ →₀ ) (b : R) (f : (σ →₀ ) →₀ R), af.supportb 0M fM ((MvPolynomial.monomial a) b)M ((let_fun this := (MvPolynomial.monomial a) b; this) + f)) (h_X : ∀ (p : MvPolynomial σ R) (n : σ), M pM (p * MvPolynomial.X n)) :
            M p

            Similar to MvPolynomial.induction_on but only a yet weaker form of h_add is required.

            theorem MvPolynomial.induction_on {R : Type u} {σ : Type u_1} [CommSemiring R] {M : MvPolynomial σ RProp} (p : MvPolynomial σ R) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add : ∀ (p q : MvPolynomial σ R), M pM qM (p + q)) (h_X : ∀ (p : MvPolynomial σ R) (n : σ), M pM (p * MvPolynomial.X n)) :
            M p

            Analog of Polynomial.induction_on.

            theorem MvPolynomial.ringHom_ext {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {f : MvPolynomial σ R →+* A} {g : MvPolynomial σ R →+* A} (hC : ∀ (r : R), f (MvPolynomial.C r) = g (MvPolynomial.C r)) (hX : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) :
            f = g
            theorem MvPolynomial.ringHom_ext' {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {f : MvPolynomial σ R →+* A} {g : MvPolynomial σ R →+* A} (hC : RingHom.comp f MvPolynomial.C = RingHom.comp g MvPolynomial.C) (hX : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) :
            f = g

            See note [partially-applied ext lemmas].

            theorem MvPolynomial.hom_eq_hom {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [Semiring S₂] (f : MvPolynomial σ R →+* S₂) (g : MvPolynomial σ R →+* S₂) (hC : RingHom.comp f MvPolynomial.C = RingHom.comp g MvPolynomial.C) (hX : ∀ (n : σ), f (MvPolynomial.X n) = g (MvPolynomial.X n)) (p : MvPolynomial σ R) :
            f p = g p
            theorem MvPolynomial.is_id {R : Type u} {σ : Type u_1} [CommSemiring R] (f : MvPolynomial σ R →+* MvPolynomial σ R) (hC : RingHom.comp f MvPolynomial.C = MvPolynomial.C) (hX : ∀ (n : σ), f (MvPolynomial.X n) = MvPolynomial.X n) (p : MvPolynomial σ R) :
            f p = p
            theorem MvPolynomial.algHom_ext' {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] {f : MvPolynomial σ A →ₐ[R] B} {g : MvPolynomial σ A →ₐ[R] B} (h₁ : AlgHom.comp f (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = AlgHom.comp g (IsScalarTower.toAlgHom R A (MvPolynomial σ A))) (h₂ : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) :
            f = g
            theorem MvPolynomial.algHom_ext {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {f : MvPolynomial σ R →ₐ[R] A} {g : MvPolynomial σ R →ₐ[R] A} (hf : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) :
            f = g
            @[simp]
            theorem MvPolynomial.algHom_C {R : Type u} {σ : Type u_1} [CommSemiring R] {τ : Type u_2} (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (r : R) :
            f (MvPolynomial.C r) = MvPolynomial.C r
            @[simp]
            theorem MvPolynomial.adjoin_range_X {R : Type u} {σ : Type u_1} [CommSemiring R] :
            Algebra.adjoin R (Set.range MvPolynomial.X) =
            theorem MvPolynomial.linearMap_ext {R : Type u} {σ : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {f : MvPolynomial σ R →ₗ[R] M} {g : MvPolynomial σ R →ₗ[R] M} (h : ∀ (s : σ →₀ ), f ∘ₗ MvPolynomial.monomial s = g ∘ₗ MvPolynomial.monomial s) :
            f = g
            def MvPolynomial.support {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :

            The finite set of all m : σ →₀ ℕ such that X^m has a non-zero coefficient.

            Equations
            Instances For
              theorem MvPolynomial.support_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [CommSemiring R] [h : Decidable (a = 0)] :
              MvPolynomial.support ((MvPolynomial.monomial s) a) = if a = 0 then else {s}
              theorem MvPolynomial.support_smul {R : Type u} {σ : Type u_1} [CommSemiring R] {S₁ : Type u_2} [SMulZeroClass S₁ R] {a : S₁} {f : MvPolynomial σ R} :
              theorem MvPolynomial.support_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq σ] {s : Finset α} {f : αMvPolynomial σ R} :
              MvPolynomial.support (Finset.sum s fun (x : α) => f x) Finset.biUnion s fun (x : α) => MvPolynomial.support (f x)
              def MvPolynomial.coeff {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (p : MvPolynomial σ R) :
              R

              The coefficient of the monomial m in the multi-variable polynomial p.

              Equations
              Instances For
                theorem MvPolynomial.sum_def {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ )RA} :
                theorem MvPolynomial.ext {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
                (∀ (m : σ →₀ ), MvPolynomial.coeff m p = MvPolynomial.coeff m q)p = q
                theorem MvPolynomial.ext_iff {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
                @[simp]
                theorem MvPolynomial.coeff_add {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
                @[simp]
                theorem MvPolynomial.coeff_smul {R : Type u} {σ : Type u_1} [CommSemiring R] {S₁ : Type u_2} [SMulZeroClass S₁ R] (m : σ →₀ ) (C : S₁) (p : MvPolynomial σ R) :
                @[simp]
                theorem MvPolynomial.coeff_zero {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) :
                @[simp]
                theorem MvPolynomial.coeff_zero_X {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) :
                def MvPolynomial.coeffAddMonoidHom {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) :

                MvPolynomial.coeff m but promoted to an AddMonoidHom.

                Equations
                Instances For
                  theorem MvPolynomial.coeff_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {X : Type u_2} (s : Finset X) (f : XMvPolynomial σ R) (m : σ →₀ ) :
                  MvPolynomial.coeff m (Finset.sum s fun (x : X) => f x) = Finset.sum s fun (x : X) => MvPolynomial.coeff m (f x)
                  theorem MvPolynomial.monic_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) :
                  (MvPolynomial.monomial m) 1 = Finsupp.prod m fun (n : σ) (e : ) => MvPolynomial.X n ^ e
                  @[simp]
                  theorem MvPolynomial.coeff_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ) (n : σ →₀ ) (a : R) :
                  MvPolynomial.coeff m ((MvPolynomial.monomial n) a) = if n = m then a else 0
                  @[simp]
                  theorem MvPolynomial.coeff_C {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ) (a : R) :
                  MvPolynomial.coeff m (MvPolynomial.C a) = if 0 = m then a else 0
                  theorem MvPolynomial.eq_C_of_isEmpty {R : Type u} {σ : Type u_1} [CommSemiring R] [IsEmpty σ] (p : MvPolynomial σ R) :
                  p = MvPolynomial.C (MvPolynomial.coeff 0 p)
                  theorem MvPolynomial.coeff_one {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ) :
                  MvPolynomial.coeff m 1 = if 0 = m then 1 else 0
                  @[simp]
                  theorem MvPolynomial.coeff_zero_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) :
                  MvPolynomial.coeff 0 (MvPolynomial.C a) = a
                  @[simp]
                  theorem MvPolynomial.coeff_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (i : σ) (m : σ →₀ ) (k : ) :
                  MvPolynomial.coeff m (MvPolynomial.X i ^ k) = if Finsupp.single i k = m then 1 else 0
                  theorem MvPolynomial.coeff_X' {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (i : σ) (m : σ →₀ ) :
                  MvPolynomial.coeff m (MvPolynomial.X i) = if Finsupp.single i 1 = m then 1 else 0
                  @[simp]
                  theorem MvPolynomial.coeff_X {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) :
                  @[simp]
                  theorem MvPolynomial.coeff_C_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (a : R) (p : MvPolynomial σ R) :
                  MvPolynomial.coeff m (MvPolynomial.C a * p) = a * MvPolynomial.coeff m p
                  theorem MvPolynomial.coeff_mul {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) (n : σ →₀ ) :
                  @[simp]
                  theorem MvPolynomial.coeff_mul_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (s : σ →₀ ) (r : R) (p : MvPolynomial σ R) :
                  @[simp]
                  theorem MvPolynomial.coeff_monomial_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (s : σ →₀ ) (r : R) (p : MvPolynomial σ R) :
                  @[simp]
                  theorem MvPolynomial.coeff_mul_X {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (s : σ) (p : MvPolynomial σ R) :
                  @[simp]
                  theorem MvPolynomial.coeff_X_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (s : σ) (p : MvPolynomial σ R) :
                  @[simp]
                  theorem MvPolynomial.support_smul_eq {R : Type u} {σ : Type u_1} [CommSemiring R] {S₁ : Type u_2} [Semiring S₁] [Module S₁ R] [NoZeroSMulDivisors S₁ R] {a : S₁} (h : a 0) (p : MvPolynomial σ R) :
                  theorem MvPolynomial.coeff_mul_monomial' {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (s : σ →₀ ) (r : R) (p : MvPolynomial σ R) :
                  MvPolynomial.coeff m (p * (MvPolynomial.monomial s) r) = if s m then MvPolynomial.coeff (m - s) p * r else 0
                  theorem MvPolynomial.coeff_monomial_mul' {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (s : σ →₀ ) (r : R) (p : MvPolynomial σ R) :
                  MvPolynomial.coeff m ((MvPolynomial.monomial s) r * p) = if s m then r * MvPolynomial.coeff (m - s) p else 0
                  theorem MvPolynomial.coeff_mul_X' {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ) (s : σ) (p : MvPolynomial σ R) :
                  MvPolynomial.coeff m (p * MvPolynomial.X s) = if s m.support then MvPolynomial.coeff (m - Finsupp.single s 1) p else 0
                  theorem MvPolynomial.coeff_X_mul' {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ) (s : σ) (p : MvPolynomial σ R) :
                  MvPolynomial.coeff m (MvPolynomial.X s * p) = if s m.support then MvPolynomial.coeff (m - Finsupp.single s 1) p else 0
                  theorem MvPolynomial.eq_zero_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} :
                  p = 0 ∀ (d : σ →₀ ), MvPolynomial.coeff d p = 0
                  theorem MvPolynomial.ne_zero_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} :
                  p 0 ∃ (d : σ →₀ ), MvPolynomial.coeff d p 0
                  @[simp]
                  theorem MvPolynomial.X_ne_zero {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (s : σ) :
                  @[simp]
                  theorem MvPolynomial.exists_coeff_ne_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} (h : p 0) :
                  ∃ (d : σ →₀ ), MvPolynomial.coeff d p 0
                  theorem MvPolynomial.C_dvd_iff_dvd_coeff {R : Type u} {σ : Type u_1} [CommSemiring R] (r : R) (φ : MvPolynomial σ R) :
                  MvPolynomial.C r φ ∀ (i : σ →₀ ), r MvPolynomial.coeff i φ
                  @[simp]
                  theorem MvPolynomial.isRegular_X {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] :
                  @[simp]
                  theorem MvPolynomial.isRegular_X_pow {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] (k : ) :
                  @[simp]
                  theorem MvPolynomial.isRegular_prod_X {R : Type u} {σ : Type u_1} [CommSemiring R] (s : Finset σ) :
                  IsRegular (Finset.prod s fun (n : σ) => MvPolynomial.X n)

                  constantCoeff p returns the constant term of the polynomial p, defined as coeff 0 p. This is a ring homomorphism.

                  Equations
                  • MvPolynomial.constantCoeff = { toMonoidHom := { toOneHom := { toFun := MvPolynomial.coeff 0, map_one' := }, map_mul' := }, map_zero' := , map_add' := }
                  Instances For
                    theorem MvPolynomial.constantCoeff_eq {R : Type u} {σ : Type u_1} [CommSemiring R] :
                    MvPolynomial.constantCoeff = MvPolynomial.coeff 0
                    @[simp]
                    theorem MvPolynomial.constantCoeff_C {R : Type u} (σ : Type u_1) [CommSemiring R] (r : R) :
                    MvPolynomial.constantCoeff (MvPolynomial.C r) = r
                    @[simp]
                    theorem MvPolynomial.constantCoeff_X (R : Type u) {σ : Type u_1} [CommSemiring R] (i : σ) :
                    MvPolynomial.constantCoeff (MvPolynomial.X i) = 0
                    @[simp]
                    theorem MvPolynomial.constantCoeff_smul {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] {R : Type u_2} [SMulZeroClass R S₁] (a : R) (f : MvPolynomial σ S₁) :
                    MvPolynomial.constantCoeff (a f) = a MvPolynomial.constantCoeff f
                    theorem MvPolynomial.constantCoeff_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (d : σ →₀ ) (r : R) :
                    MvPolynomial.constantCoeff ((MvPolynomial.monomial d) r) = if d = 0 then r else 0
                    @[simp]
                    theorem MvPolynomial.constantCoeff_comp_C (R : Type u) (σ : Type u_1) [CommSemiring R] :
                    RingHom.comp MvPolynomial.constantCoeff MvPolynomial.C = RingHom.id R
                    @[simp]
                    theorem MvPolynomial.constantCoeff_comp_algebraMap (R : Type u) (σ : Type u_1) [CommSemiring R] :
                    RingHom.comp MvPolynomial.constantCoeff (algebraMap R (MvPolynomial σ R)) = RingHom.id R
                    def MvPolynomial.eval₂ {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (p : MvPolynomial σ R) :
                    S₁

                    Evaluate a polynomial p given a valuation g of all the variables and a ring hom f from the scalar ring to the target

                    Equations
                    Instances For
                      theorem MvPolynomial.eval₂_eq {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (g : R →+* S₁) (X : σS₁) (f : MvPolynomial σ R) :
                      MvPolynomial.eval₂ g X f = Finset.sum (MvPolynomial.support f) fun (d : σ →₀ ) => g (MvPolynomial.coeff d f) * Finset.prod d.support fun (i : σ) => X i ^ d i
                      theorem MvPolynomial.eval₂_eq' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Fintype σ] (g : R →+* S₁) (X : σS₁) (f : MvPolynomial σ R) :
                      MvPolynomial.eval₂ g X f = Finset.sum (MvPolynomial.support f) fun (d : σ →₀ ) => g (MvPolynomial.coeff d f) * Finset.prod Finset.univ fun (i : σ) => X i ^ d i
                      @[simp]
                      theorem MvPolynomial.eval₂_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) :
                      @[simp]
                      theorem MvPolynomial.eval₂_add {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (f : R →+* S₁) (g : σS₁) :
                      @[simp]
                      theorem MvPolynomial.eval₂_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ } [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) :
                      MvPolynomial.eval₂ f g ((MvPolynomial.monomial s) a) = f a * Finsupp.prod s fun (n : σ) (e : ) => g n ^ e
                      @[simp]
                      theorem MvPolynomial.eval₂_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (a : R) :
                      MvPolynomial.eval₂ f g (MvPolynomial.C a) = f a
                      @[simp]
                      theorem MvPolynomial.eval₂_one {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) :
                      @[simp]
                      theorem MvPolynomial.eval₂_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (n : σ) :
                      theorem MvPolynomial.eval₂_mul_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g : σS₁) {s : σ →₀ } {a : R} :
                      MvPolynomial.eval₂ f g (p * (MvPolynomial.monomial s) a) = MvPolynomial.eval₂ f g p * f a * Finsupp.prod s fun (n : σ) (e : ) => g n ^ e
                      theorem MvPolynomial.eval₂_mul_C {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g : σS₁) :
                      MvPolynomial.eval₂ f g (p * MvPolynomial.C a) = MvPolynomial.eval₂ f g p * f a
                      @[simp]
                      theorem MvPolynomial.eval₂_mul {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {q : MvPolynomial σ R} (f : R →+* S₁) (g : σS₁) {p : MvPolynomial σ R} :
                      @[simp]
                      theorem MvPolynomial.eval₂_pow {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) {p : MvPolynomial σ R} {n : } :
                      def MvPolynomial.eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) :

                      MvPolynomial.eval₂ as a RingHom.

                      Equations
                      Instances For
                        @[simp]
                        theorem MvPolynomial.coe_eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) :
                        theorem MvPolynomial.eval₂Hom_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f₁ : R →+* S₁} {f₂ : R →+* S₁} {g₁ : σS₁} {g₂ : σS₁} {p₁ : MvPolynomial σ R} {p₂ : MvPolynomial σ R} :
                        f₁ = f₂g₁ = g₂p₁ = p₂(MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂
                        @[simp]
                        theorem MvPolynomial.eval₂Hom_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (r : R) :
                        (MvPolynomial.eval₂Hom f g) (MvPolynomial.C r) = f r
                        @[simp]
                        theorem MvPolynomial.eval₂Hom_X' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (i : σ) :
                        @[simp]
                        theorem MvPolynomial.comp_eval₂Hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σS₁) (φ : S₁ →+* S₂) :
                        theorem MvPolynomial.map_eval₂Hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σS₁) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
                        φ ((MvPolynomial.eval₂Hom f g) p) = (MvPolynomial.eval₂Hom (RingHom.comp φ f) fun (i : σ) => φ (g i)) p
                        theorem MvPolynomial.eval₂Hom_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (d : σ →₀ ) (r : R) :
                        (MvPolynomial.eval₂Hom f g) ((MvPolynomial.monomial d) r) = f r * Finsupp.prod d fun (i : σ) (k : ) => g i ^ k
                        theorem MvPolynomial.eval₂_comp_left {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {S₂ : Type u_2} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σS₁) (p : MvPolynomial σ R) :
                        @[simp]
                        theorem MvPolynomial.eval₂_eta {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
                        MvPolynomial.eval₂ MvPolynomial.C MvPolynomial.X p = p
                        theorem MvPolynomial.eval₂_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g₁ : σS₁) (g₂ : σS₁) (h : ∀ {i : σ} {c : σ →₀ }, i c.supportMvPolynomial.coeff c p 0g₁ i = g₂ i) :
                        @[simp]
                        theorem MvPolynomial.eval₂_sum {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (s : Finset S₂) (p : S₂MvPolynomial σ R) :
                        MvPolynomial.eval₂ f g (Finset.sum s fun (x : S₂) => p x) = Finset.sum s fun (x : S₂) => MvPolynomial.eval₂ f g (p x)
                        @[simp]
                        theorem MvPolynomial.eval₂_prod {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (s : Finset S₂) (p : S₂MvPolynomial σ R) :
                        MvPolynomial.eval₂ f g (Finset.prod s fun (x : S₂) => p x) = Finset.prod s fun (x : S₂) => MvPolynomial.eval₂ f g (p x)
                        theorem MvPolynomial.eval₂_assoc {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (q : S₂MvPolynomial σ R) (p : MvPolynomial S₂ R) :
                        MvPolynomial.eval₂ f (fun (t : S₂) => MvPolynomial.eval₂ f g (q t)) p = MvPolynomial.eval₂ f g (MvPolynomial.eval₂ MvPolynomial.C q p)
                        def MvPolynomial.eval {R : Type u} {σ : Type u_1} [CommSemiring R] (f : σR) :

                        Evaluate a polynomial p given a valuation f of all the variables

                        Equations
                        Instances For
                          theorem MvPolynomial.eval_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (X : σR) (f : MvPolynomial σ R) :
                          (MvPolynomial.eval X) f = Finset.sum (MvPolynomial.support f) fun (d : σ →₀ ) => MvPolynomial.coeff d f * Finset.prod d.support fun (i : σ) => X i ^ d i
                          theorem MvPolynomial.eval_eq' {R : Type u} {σ : Type u_1} [CommSemiring R] [Fintype σ] (X : σR) (f : MvPolynomial σ R) :
                          (MvPolynomial.eval X) f = Finset.sum (MvPolynomial.support f) fun (d : σ →₀ ) => MvPolynomial.coeff d f * Finset.prod Finset.univ fun (i : σ) => X i ^ d i
                          theorem MvPolynomial.eval_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [CommSemiring R] {f : σR} :
                          (MvPolynomial.eval f) ((MvPolynomial.monomial s) a) = a * Finsupp.prod s fun (n : σ) (e : ) => f n ^ e
                          @[simp]
                          theorem MvPolynomial.eval_C {R : Type u} {σ : Type u_1} [CommSemiring R] {f : σR} (a : R) :
                          (MvPolynomial.eval f) (MvPolynomial.C a) = a
                          @[simp]
                          theorem MvPolynomial.eval_X {R : Type u} {σ : Type u_1} [CommSemiring R] {f : σR} (n : σ) :
                          @[simp]
                          theorem MvPolynomial.smul_eval {R : Type u} {σ : Type u_1} [CommSemiring R] (x : σR) (p : MvPolynomial σ R) (s : R) :
                          theorem MvPolynomial.eval_add {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} {f : σR} :
                          theorem MvPolynomial.eval_mul {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} {f : σR} :
                          theorem MvPolynomial.eval_pow {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {f : σR} (n : ) :
                          theorem MvPolynomial.eval_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ιMvPolynomial σ R) (g : σR) :
                          (MvPolynomial.eval g) (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => (MvPolynomial.eval g) (f i)
                          theorem MvPolynomial.eval_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ιMvPolynomial σ R) (g : σR) :
                          (MvPolynomial.eval g) (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => (MvPolynomial.eval g) (f i)
                          theorem MvPolynomial.eval_assoc {R : Type u} {σ : Type u_1} [CommSemiring R] {τ : Type u_2} (f : σMvPolynomial τ R) (g : τR) (p : MvPolynomial σ R) :
                          @[simp]
                          theorem MvPolynomial.eval₂_id {R : Type u} {σ : Type u_1} [CommSemiring R] {g : σR} (p : MvPolynomial σ R) :
                          theorem MvPolynomial.eval_eval₂ {R : Type u} {σ : Type u_1} {S : Type u_2} {τ : Type u_3} {x : τS} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial τ S) (g : σMvPolynomial τ S) (p : MvPolynomial σ R) :
                          def MvPolynomial.map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) :

                          map f p maps a polynomial p across a ring hom f

                          Equations
                          Instances For
                            @[simp]
                            theorem MvPolynomial.map_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (s : σ →₀ ) (a : R) :
                            @[simp]
                            theorem MvPolynomial.map_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (a : R) :
                            (MvPolynomial.map f) (MvPolynomial.C a) = MvPolynomial.C (f a)
                            @[simp]
                            theorem MvPolynomial.map_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (n : σ) :
                            theorem MvPolynomial.map_id {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
                            theorem MvPolynomial.map_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) [CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R) :
                            theorem MvPolynomial.eval₂_eq_eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (p : MvPolynomial σ R) :
                            theorem MvPolynomial.eval₂_comp_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {S₂ : Type u_2} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σS₁) (p : MvPolynomial σ R) :
                            theorem MvPolynomial.map_eval₂ {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : S₂MvPolynomial S₃ R) (p : MvPolynomial S₂ R) :
                            (MvPolynomial.map f) (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C ((MvPolynomial.map f) g) ((MvPolynomial.map f) p)
                            theorem MvPolynomial.coeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (p : MvPolynomial σ R) (m : σ →₀ ) :
                            theorem MvPolynomial.map_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (hf : Function.Injective f) :
                            theorem MvPolynomial.map_surjective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (hf : Function.Surjective f) :
                            theorem MvPolynomial.map_leftInverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.LeftInverse f g) :

                            If f is a left-inverse of g then map f is a left-inverse of map g.

                            theorem MvPolynomial.map_rightInverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.RightInverse f g) :

                            If f is a right-inverse of g then map f is a right-inverse of map g.

                            @[simp]
                            theorem MvPolynomial.eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σS₁) (p : MvPolynomial σ R) :
                            @[simp]
                            theorem MvPolynomial.eval₂_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σS₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
                            @[simp]
                            theorem MvPolynomial.eval₂Hom_map_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σS₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) :
                            @[simp]
                            theorem MvPolynomial.constantCoeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (φ : MvPolynomial σ R) :
                            MvPolynomial.constantCoeff ((MvPolynomial.map f) φ) = f (MvPolynomial.constantCoeff φ)
                            theorem MvPolynomial.constantCoeff_comp_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) :
                            RingHom.comp MvPolynomial.constantCoeff (MvPolynomial.map f) = RingHom.comp f MvPolynomial.constantCoeff
                            theorem MvPolynomial.C_dvd_iff_map_hom_eq_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (q : R →+* S₁) (r : R) (hr : ∀ (r' : R), q r' = 0 r r') (φ : MvPolynomial σ R) :
                            MvPolynomial.C r φ (MvPolynomial.map q) φ = 0
                            theorem MvPolynomial.map_mapRange_eq_iff {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : S₁R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁) :
                            (MvPolynomial.map f) (Finsupp.mapRange g hg φ) = φ ∀ (d : σ →₀ ), f (g (MvPolynomial.coeff d φ)) = MvPolynomial.coeff d φ
                            @[simp]
                            theorem MvPolynomial.mapAlgHom_apply {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) (p : MvPolynomial σ S₁) :
                            (MvPolynomial.mapAlgHom f) p = MvPolynomial.eval₂ (RingHom.comp MvPolynomial.C f) MvPolynomial.X p
                            def MvPolynomial.mapAlgHom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :

                            If f : S₁ →ₐ[R] S₂ is a morphism of R-algebras, then so is MvPolynomial.map f.

                            Equations
                            Instances For
                              @[simp]
                              theorem MvPolynomial.mapAlgHom_id {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] :
                              @[simp]
                              theorem MvPolynomial.mapAlgHom_coe_ringHom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :

                              The algebra of multivariate polynomials #

                              theorem MvPolynomial.algebraMap_apply {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (r : R) :
                              (algebraMap R (MvPolynomial σ S₁)) r = MvPolynomial.C ((algebraMap R S₁) r)
                              def MvPolynomial.aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) :

                              A map σ → S₁ where S₁ is an algebra over R generates an R-algebra homomorphism from multivariate polynomials over σ to S₁.

                              Equations
                              Instances For
                                theorem MvPolynomial.aeval_def {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) (p : MvPolynomial σ R) :
                                theorem MvPolynomial.aeval_eq_eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) (p : MvPolynomial σ R) :
                                @[simp]
                                theorem MvPolynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) (s : σ) :
                                @[simp]
                                theorem MvPolynomial.aeval_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) (r : R) :
                                (MvPolynomial.aeval f) (MvPolynomial.C r) = (algebraMap R S₁) r
                                theorem MvPolynomial.aeval_unique {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (φ : MvPolynomial σ R →ₐ[R] S₁) :
                                φ = MvPolynomial.aeval (φ MvPolynomial.X)
                                theorem MvPolynomial.aeval_X_left {R : Type u} {σ : Type u_1} [CommSemiring R] :
                                MvPolynomial.aeval MvPolynomial.X = AlgHom.id R (MvPolynomial σ R)
                                theorem MvPolynomial.aeval_X_left_apply {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
                                (MvPolynomial.aeval MvPolynomial.X) p = p
                                theorem MvPolynomial.comp_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) {B : Type u_2} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) :
                                AlgHom.comp φ (MvPolynomial.aeval f) = MvPolynomial.aeval fun (i : σ) => φ (f i)
                                @[simp]
                                theorem MvPolynomial.map_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] {B : Type u_2} [CommSemiring B] (g : σS₁) (φ : S₁ →+* B) (p : MvPolynomial σ R) :
                                φ ((MvPolynomial.aeval g) p) = (MvPolynomial.eval₂Hom (RingHom.comp φ (algebraMap R S₁)) fun (i : σ) => φ (g i)) p
                                @[simp]
                                theorem MvPolynomial.eval₂Hom_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) :
                                MvPolynomial.eval₂Hom f 0 = RingHom.comp f MvPolynomial.constantCoeff
                                @[simp]
                                theorem MvPolynomial.eval₂Hom_zero' {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) :
                                (MvPolynomial.eval₂Hom f fun (x : σ) => 0) = RingHom.comp f MvPolynomial.constantCoeff
                                theorem MvPolynomial.eval₂Hom_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) :
                                (MvPolynomial.eval₂Hom f 0) p = f (MvPolynomial.constantCoeff p)
                                theorem MvPolynomial.eval₂Hom_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) :
                                (MvPolynomial.eval₂Hom f fun (x : σ) => 0) p = f (MvPolynomial.constantCoeff p)
                                @[simp]
                                theorem MvPolynomial.eval₂_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) :
                                MvPolynomial.eval₂ f 0 p = f (MvPolynomial.constantCoeff p)
                                @[simp]
                                theorem MvPolynomial.eval₂_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) :
                                MvPolynomial.eval₂ f (fun (x : σ) => 0) p = f (MvPolynomial.constantCoeff p)
                                @[simp]
                                theorem MvPolynomial.aeval_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (p : MvPolynomial σ R) :
                                (MvPolynomial.aeval 0) p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)
                                @[simp]
                                theorem MvPolynomial.aeval_zero' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (p : MvPolynomial σ R) :
                                (MvPolynomial.aeval fun (x : σ) => 0) p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)
                                @[simp]
                                theorem MvPolynomial.eval_zero {R : Type u} {σ : Type u_1} [CommSemiring R] :
                                MvPolynomial.eval 0 = MvPolynomial.constantCoeff
                                @[simp]
                                theorem MvPolynomial.eval_zero' {R : Type u} {σ : Type u_1} [CommSemiring R] :
                                (MvPolynomial.eval fun (x : σ) => 0) = MvPolynomial.constantCoeff
                                theorem MvPolynomial.aeval_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (g : σS₁) (d : σ →₀ ) (r : R) :
                                (MvPolynomial.aeval g) ((MvPolynomial.monomial d) r) = (algebraMap R S₁) r * Finsupp.prod d fun (i : σ) (k : ) => g i ^ k
                                theorem MvPolynomial.eval₂Hom_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (g : σS₂) (φ : MvPolynomial σ R) (h : ∀ (d : σ →₀ ), MvPolynomial.coeff d φ 0∃ i ∈ d.support, g i = 0) :
                                theorem MvPolynomial.aeval_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] [Algebra R S₂] (f : σS₂) (φ : MvPolynomial σ R) (h : ∀ (d : σ →₀ ), MvPolynomial.coeff d φ 0∃ i ∈ d.support, f i = 0) :
                                theorem MvPolynomial.aeval_sum {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) {ι : Type u_2} (s : Finset ι) (φ : ιMvPolynomial σ R) :
                                (MvPolynomial.aeval f) (Finset.sum s fun (i : ι) => φ i) = Finset.sum s fun (i : ι) => (MvPolynomial.aeval f) (φ i)
                                theorem MvPolynomial.aeval_prod {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) {ι : Type u_2} (s : Finset ι) (φ : ιMvPolynomial σ R) :
                                (MvPolynomial.aeval f) (Finset.prod s fun (i : ι) => φ i) = Finset.prod s fun (i : ι) => (MvPolynomial.aeval f) (φ i)
                                theorem Algebra.adjoin_range_eq_range_aeval (R : Type u) {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) :
                                theorem Algebra.adjoin_eq_range (R : Type u) {S₁ : Type v} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (s : Set S₁) :
                                def MvPolynomial.aevalTower {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (f : R →ₐ[S] A) (X : σA) :

                                Version of aeval for defining algebra homs out of MvPolynomial σ R over a smaller base ring than R.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem MvPolynomial.aevalTower_X {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) (i : σ) :
                                  @[simp]
                                  theorem MvPolynomial.aevalTower_C {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) (x : R) :
                                  (MvPolynomial.aevalTower g y) (MvPolynomial.C x) = g x
                                  @[simp]
                                  theorem MvPolynomial.aevalTower_comp_C {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) :
                                  RingHom.comp ((MvPolynomial.aevalTower g y)) MvPolynomial.C = g
                                  @[simp]
                                  theorem MvPolynomial.aevalTower_algebraMap {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) (x : R) :
                                  @[simp]
                                  theorem MvPolynomial.aevalTower_comp_algebraMap {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) :
                                  theorem MvPolynomial.aevalTower_toAlgHom {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) (x : R) :
                                  @[simp]
                                  theorem MvPolynomial.aevalTower_comp_toAlgHom {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) :
                                  @[simp]
                                  theorem MvPolynomial.aevalTower_id {σ : Type u_1} {S : Type u_2} [CommSemiring S] :
                                  MvPolynomial.aevalTower (AlgHom.id S S) = MvPolynomial.aeval
                                  @[simp]
                                  theorem MvPolynomial.aevalTower_ofId {σ : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S A] :
                                  MvPolynomial.aevalTower (Algebra.ofId S A) = MvPolynomial.aeval
                                  theorem MvPolynomial.eval₂_mem {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {subS : Type u_3} [CommSemiring S] [SetLike subS S] [SubsemiringClass subS S] {f : R →+* S} {p : MvPolynomial σ R} {s : subS} (hs : iMvPolynomial.support p, f (MvPolynomial.coeff i p) s) {v : σS} (hv : ∀ (i : σ), v i s) :
                                  theorem MvPolynomial.eval_mem {σ : Type u_1} {S : Type u_2} {subS : Type u_3} [CommSemiring S] [SetLike subS S] [SubsemiringClass subS S] {p : MvPolynomial σ S} {s : subS} (hs : iMvPolynomial.support p, MvPolynomial.coeff i p s) {v : σS} (hv : ∀ (i : σ), v i s) :