R : Type u_1
inst✝ : Semiring R
⊢ ↑(MvPowerSeries.coeff R 0) = ↑(constantCoeff R)
R : Type u_1
inst✝ : Semiring R
⊢ ↑(coeff R 0) = ↑(constantCoeff R)
rw [coeff, Finsupp.single_zero]
no goals
R : Type u_1
inst✝ : Semiring R
⊢ ↑(MvPowerSeries.coeff R 0) = ↑(constantCoeff R)
rfl