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
inst✝ : DecidableEq σ
d : σ →₀ ℕ
r : R
⊢ ↑constantCoeff (↑(monomial d) r) = if d = 0 then r else 0
rw [constantCoeff_eq, coeff_monomial]