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.decidableEq
    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.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.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.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.single_eq_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ) (a : R) :
      (fun₀ | s => a) = ↑(MvPolynomial.monomial s) a
      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 => Finsupp.sum q fun n b => ↑(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
          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] :
          ↑(MvPolynomial.monomial s) a ^ e = ↑(MvPolynomial.monomial (e s)) (a ^ e)
          @[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
            @[simp]
            theorem MvPolynomial.X_pow_eq_monomial {R : Type u} {σ : Type u_1} {e : } {n : σ} [CommSemiring R] :
            MvPolynomial.X n ^ e = ↑(MvPolynomial.monomial fun₀ | n => e) 1
            theorem MvPolynomial.monomial_add_single {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ } [CommSemiring R] :
            ↑(MvPolynomial.monomial (s + fun₀ | n => e)) a = ↑(MvPolynomial.monomial s) a * MvPolynomial.X n ^ e
            theorem MvPolynomial.monomial_single_add {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ } [CommSemiring R] :
            ↑(MvPolynomial.monomial ((fun₀ | n => e) + s)) a = MvPolynomial.X n ^ e * ↑(MvPolynomial.monomial s) a
            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 fun₀ | s => n) a
            theorem MvPolynomial.C_mul_X_eq_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ} {a : R} :
            MvPolynomial.C a * MvPolynomial.X s = ↑(MvPolynomial.monomial fun₀ | s => 1) a
            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} :
            ↑(MvPolynomial.monomial s) b = 0 b = 0
            @[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
            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) → ¬a f.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) → ¬a f.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] (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 : σ →₀ ), LinearMap.comp f (MvPolynomial.monomial s) = LinearMap.comp 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_X {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] [Nontrivial R] :
              MvPolynomial.support (MvPolynomial.X n) = {fun₀ | n => 1}
              theorem MvPolynomial.support_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (s : σ) (n : ) :
              MvPolynomial.support (MvPolynomial.X s ^ n) = {fun₀ | 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} :
              theorem MvPolynomial.support_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq σ] {s : Finset α} {f : αMvPolynomial σ R} :
              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
                • One or more equations did not get rendered due to their size.
                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 => f x) = Finset.sum s fun x => MvPolynomial.coeff m (f x)
                  theorem MvPolynomial.monic_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ) :
                  @[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
                  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 (fun₀ | 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 (fun₀ | i => 1) = m then 1 else 0
                  @[simp]
                  theorem MvPolynomial.coeff_X {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) :
                  MvPolynomial.coeff (fun₀ | i => 1) (MvPolynomial.X i) = 1
                  @[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) :
                  MvPolynomial.coeff ((fun₀ | s => 1) + m) (MvPolynomial.X s * p) = MvPolynomial.coeff m p
                  @[simp]
                  @[simp]
                  @[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 - fun₀ | 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 - fun₀ | 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.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 σ) :

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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
                      • One or more equations did not get rendered due to their size.
                      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 => p x) = Finset.sum s fun x => 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 => p x) = Finset.prod s fun x => 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 => 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) :
                          ↑(MvPolynomial.eval x) (s p) = s * ↑(MvPolynomial.eval x) p
                          theorem MvPolynomial.eval_add {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} {f : σR} :
                          ↑(MvPolynomial.eval f) (p + q) = ↑(MvPolynomial.eval f) p + ↑(MvPolynomial.eval f) q
                          theorem MvPolynomial.eval_mul {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} {f : σR} :
                          ↑(MvPolynomial.eval f) (p * q) = ↑(MvPolynomial.eval f) p * ↑(MvPolynomial.eval f) q
                          theorem MvPolynomial.eval_pow {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {f : σR} (n : ) :
                          ↑(MvPolynomial.eval f) (p ^ n) = ↑(MvPolynomial.eval f) p ^ 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) :
                          ↑(MvPolynomial.eval (↑(MvPolynomial.eval g) f)) p = ↑(MvPolynomial.eval g) (MvPolynomial.eval₂ MvPolynomial.C f p)
                          @[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
                            • One or more equations did not get rendered due to their size.
                            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
                              • One or more equations did not get rendered due to their size.
                              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) :
                                @[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 ((fun x => R) p) 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 ((fun x => R) p) 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 φ 0i, 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 φ 0i, i d.support f i = 0) :
                                ↑(MvPolynomial.aeval f) φ = 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
                                • One or more equations did not get rendered due to their size.
                                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) :
                                  ↑(MvPolynomial.aevalTower g y) (↑(algebraMap R (MvPolynomial σ R)) x) = g x
                                  @[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) :
                                  ↑(MvPolynomial.aevalTower g y) (↑(IsScalarTower.toAlgHom S R (MvPolynomial σ R)) x) = g x
                                  @[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 : ∀ (i : σ →₀ ), i MvPolynomial.support pf (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 : ∀ (i : σ →₀ ), i MvPolynomial.support pMvPolynomial.coeff i p s) {v : σS} (hv : ∀ (i : σ), v i s) :