Documentation

Mathlib.Algebra.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
      • MvPolynomial.C = { toFun := (MvPolynomial.monomial 0), map_one' := , map_mul' := , map_zero' := , map_add' := }
      Instances For
        @[simp]
        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 (∑ is, f i)) 1 = is, (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 (∑ is, f i)) a = MvPolynomial.C a * is, (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 (f.sum g)) a = MvPolynomial.C a * f.prod 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 * s.prod fun (n : σ) (e : ) => MvPolynomial.X n ^ e
            @[simp]
            theorem MvPolynomial.prod_X_pow_eq_monomial {R : Type u} {σ : Type u_1} {s : σ →₀ } [CommSemiring R] :
            xs.support, 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'_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {f : MvPolynomial σ R →+* A} {g : MvPolynomial σ R →+* A} :
            f = g f.comp MvPolynomial.C = g.comp MvPolynomial.C ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)
            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 : f.comp MvPolynomial.C = g.comp 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 : f.comp MvPolynomial.C = g.comp 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 : f.comp MvPolynomial.C = MvPolynomial.C) (hX : ∀ (n : σ), f (MvPolynomial.X n) = MvPolynomial.X n) (p : MvPolynomial σ R) :
            f p = p
            theorem MvPolynomial.algHom_ext'_iff {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} :
            f = g f.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = g.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)
            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₁ : f.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = g.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A))) (h₂ : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) :
            f = g
            theorem MvPolynomial.algHom_ext_iff {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} :
            f = g ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)
            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] {A : Type u_2} [Semiring A] [Algebra R A] (f : MvPolynomial σ R →ₐ[R] A) (r : R) :
            f (MvPolynomial.C r) = (algebraMap R A) 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_iff {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} :
            f = g ∀ (s : σ →₀ ), f ∘ₗ MvPolynomial.monomial s = g ∘ₗ MvPolynomial.monomial s
            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
            • p.support = p.support
            Instances For
              theorem MvPolynomial.finsupp_support_eq_support {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
              p.support = p.support
              theorem MvPolynomial.support_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [CommSemiring R] [h : Decidable (a = 0)] :
              ((MvPolynomial.monomial s) a).support = if a = 0 then else {s}
              theorem MvPolynomial.support_monomial_subset {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [CommSemiring R] :
              ((MvPolynomial.monomial s) a).support {s}
              theorem MvPolynomial.support_add {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} [DecidableEq σ] :
              (p + q).support p.support q.support
              theorem MvPolynomial.support_X {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] [Nontrivial R] :
              (MvPolynomial.X n).support = {Finsupp.single n 1}
              theorem MvPolynomial.support_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (s : σ) (n : ) :
              (MvPolynomial.X s ^ n).support = {Finsupp.single s n}
              theorem MvPolynomial.support_smul {R : Type u} {σ : Type u_1} [CommSemiring R] {S₁ : Type u_2} [SMulZeroClass S₁ R] {a : S₁} {f : MvPolynomial σ R} :
              (a f).support f.support
              theorem MvPolynomial.support_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq σ] {s : Finset α} {f : αMvPolynomial σ R} :
              (∑ xs, f x).support s.biUnion fun (x : α) => (f x).support
              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
                @[simp]
                theorem MvPolynomial.mem_support_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ } :
                m p.support MvPolynomial.coeff m p 0
                theorem MvPolynomial.not_mem_support_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ } :
                mp.support MvPolynomial.coeff m p = 0
                theorem MvPolynomial.sum_def {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ )RA} :
                Finsupp.sum p b = mp.support, b m (MvPolynomial.coeff m p)
                theorem MvPolynomial.support_mul {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
                (p * q).support p.support + q.support
                theorem MvPolynomial.ext_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} :
                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
                @[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
                  @[simp]
                  theorem MvPolynomial.lcoeff_apply (R : Type u) {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) (p : MvPolynomial σ R) :
                  def MvPolynomial.lcoeff (R : Type u) {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) :

                  MvPolynomial.coeff m but promoted to a LinearMap.

                  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 (∑ xs, f x) = xs, MvPolynomial.coeff m (f x)
                    theorem MvPolynomial.monic_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) :
                    (MvPolynomial.monomial m) 1 = m.prod 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) :
                    theorem MvPolynomial.coeff_single_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (s : σ) (s' : σ) (n : ) (n' : ) :
                    MvPolynomial.coeff (Finsupp.single s' n') (MvPolynomial.X s ^ n) = if s = s' n = n' n = 0 n' = 0 then 1 else 0
                    @[simp]
                    theorem MvPolynomial.coeff_single_X {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (s : σ) (s' : σ) (n : ) :
                    MvPolynomial.coeff (Finsupp.single s' n) (MvPolynomial.X s) = if n = 1 s = s' then 1 else 0
                    @[simp]
                    theorem MvPolynomial.support_mul_X {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ) (p : MvPolynomial σ R) :
                    @[simp]
                    theorem MvPolynomial.support_X_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (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) :
                    (a p).support = p.support
                    theorem MvPolynomial.support_sdiff_support_subset_support_add {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
                    p.support \ q.support (p + q).support
                    theorem MvPolynomial.support_symmDiff_support_subset_support_add {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
                    symmDiff p.support q.support (p + q).support
                    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.support_eq_empty {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} :
                    p.support = p = 0
                    @[simp]
                    theorem MvPolynomial.support_nonempty {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} :
                    p.support.Nonempty p 0
                    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 (∏ ns, MvPolynomial.X n)
                    def MvPolynomial.coeffs {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :

                    The finset of nonzero coefficients of a multivariate polynomial.

                    Equations
                    Instances For
                      theorem MvPolynomial.mem_coeffs_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {c : R} :
                      c p.coeffs np.support, c = MvPolynomial.coeff n p
                      theorem MvPolynomial.coeff_mem_coeffs {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} (m : σ →₀ ) (h : MvPolynomial.coeff m p 0) :
                      MvPolynomial.coeff m p p.coeffs
                      theorem MvPolynomial.zero_not_mem_coeffs {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
                      0p.coeffs

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

                      Equations
                      • MvPolynomial.constantCoeff = { 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] :
                        MvPolynomial.constantCoeff.comp MvPolynomial.C = RingHom.id R
                        theorem MvPolynomial.constantCoeff_comp_algebraMap (R : Type u) (σ : Type u_1) [CommSemiring R] :
                        MvPolynomial.constantCoeff.comp (algebraMap R (MvPolynomial σ R)) = RingHom.id R
                        @[simp]
                        theorem MvPolynomial.support_sum_monomial_coeff {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
                        vp.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v p) = p
                        theorem MvPolynomial.as_sum {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
                        p = vp.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v p)
                        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 = df.support, g (MvPolynomial.coeff d f) * id.support, 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 = df.support, g (MvPolynomial.coeff d f) * 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 * s.prod 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 * s.prod 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₂) :
                            φ.comp (MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂Hom (φ.comp f) fun (i : σ) => φ (g i)
                            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 (φ.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 * d.prod 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) :
                            k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ (k.comp f) (k g) p
                            @[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 (∑ xs, p x) = xs, 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 (∏ xs, p x) = xs, 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 = df.support, MvPolynomial.coeff d f * id.support, 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 = df.support, MvPolynomial.coeff d f * 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 * s.prod 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) (∑ is, f i) = is, (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) (∏ is, f i) = is, (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} [CommSemiring R] {S : Type u_2} {τ : Type u_3} {x : τS} [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₁) :
                                MvPolynomial.constantCoeff.comp (MvPolynomial.map f) = f.comp MvPolynomial.constantCoeff
                                theorem MvPolynomial.support_map_subset {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (p : MvPolynomial σ R) :
                                ((MvPolynomial.map f) p).support p.support
                                theorem MvPolynomial.support_map_of_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (p : MvPolynomial σ R) {f : R →+* S₁} (hf : Function.Injective f) :
                                ((MvPolynomial.map f) p).support = p.support
                                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₂ (MvPolynomial.C.comp 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 #

                                  @[simp]
                                  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.coe_aeval_eq_eval {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] (f : σS₁) :
                                    @[simp]
                                    theorem MvPolynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σS₁) (s : σ) :
                                    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) :
                                    φ.comp (MvPolynomial.aeval f) = MvPolynomial.aeval fun (i : σ) => φ (f i)
                                    theorem MvPolynomial.comp_aeval_apply {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) (p : MvPolynomial σ R) :
                                    φ ((MvPolynomial.aeval f) p) = (MvPolynomial.aeval fun (i : σ) => φ (f i)) p
                                    @[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 (φ.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 = f.comp 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) = f.comp 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 * d.prod 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 φ 0id.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 φ 0id.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) (∑ is, φ i) = is, (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) (∏ is, φ i) = is, (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₁) :
                                    Algebra.adjoin R s = (MvPolynomial.aeval Subtype.val).range
                                    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) :
                                      (↑(MvPolynomial.aevalTower g y)).comp MvPolynomial.C = g
                                      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) :
                                      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) :
                                      (↑(MvPolynomial.aevalTower g y)).comp (algebraMap R (MvPolynomial σ R)) = g
                                      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 : ip.support, 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 : ip.support, MvPolynomial.coeff i p s) {v : σS} (hv : ∀ (i : σ), v i s) :
                                      theorem MvPolynomial.aeval_sum_elim {R : Type u} [CommSemiring R] {S : Type u_2} {T : Type u_3} [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {σ : Type u_4} {τ : Type u_5} (p : MvPolynomial (σ τ) R) (f : τS) (g : σT) :
                                      (MvPolynomial.aeval (Sum.elim g ((algebraMap S T) f))) p = (MvPolynomial.aeval g) ((MvPolynomial.aeval (Sum.elim MvPolynomial.X (MvPolynomial.C f))) p)