R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type ?u.315261
a✝ a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
inst✝³ : CommSemiring R✝
inst✝² : CommSemiring S₁
p✝ q : MvPolynomial σ✝ R✝
R : Type u_1
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ ↑(↑C (toFun p 0)) a = ↑p a
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type ?u.315261
a a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
inst✝³ : CommSemiring R✝
inst✝² : CommSemiring S₁
p q : MvPolynomial σ✝ R✝
R : Type u_1
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : IsEmpty σ
⊢ Surjective ↑C
refine' fun p => ⟨p.toFun 0, Finsupp.ext fun a => _⟩
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type ?u.315261
a✝ a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
inst✝³ : CommSemiring R✝
inst✝² : CommSemiring S₁
p✝ q : MvPolynomial σ✝ R✝
R : Type u_1
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ toFun p 0 = ↑p 0
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type ?u.315261
a✝ a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
inst✝³ : CommSemiring R✝
inst✝² : CommSemiring S₁
p✝ q : MvPolynomial σ✝ R✝
R : Type u_1
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ ↑(↑C (toFun p 0)) a = ↑p a
simp only [C_apply, ←single_eq_monomial, (Finsupp.ext isEmptyElim (α := σ) : a = 0),
  single_eq_same]
no goals
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type ?u.315261
a✝ a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
inst✝³ : CommSemiring R✝
inst✝² : CommSemiring S₁
p✝ q : MvPolynomial σ✝ R✝
R : Type u_1
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ toFun p 0 = ↑p 0
rfl