R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
f✝ : R →+* S₁
g✝ : σ → S₁
inst✝ : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ ∑ x in support f, ↑g (coeff x f) * ∏ x_1 in x.support, X x_1 ^ ↑x x_1 =
    ∑ x in support f, ↑g (coeff x f) * Finsupp.prod x fun a b => X a ^ b
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
f✝ : R →+* S₁
g✝ : σ → S₁
inst✝ : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ eval₂ g X f = ∑ d in support f, ↑g (coeff d f) * ∏ i : σ, X i ^ ↑d i
simp only [eval₂_eq, ← Finsupp.prod_pow]
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
p q : MvPolynomial σ R
f✝ : R →+* S₁
g✝ : σ → S₁
inst✝ : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ ∑ x in support f, ↑g (coeff x f) * ∏ x_1 in x.support, X x_1 ^ ↑x x_1 =
    ∑ x in support f, ↑g (coeff x f) * Finsupp.prod x fun a b => X a ^ b
rfl