case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
n✝ : σ →₀ ℕ
⊢ ↑(coeff R n✝) (a • f) = ↑(coeff R n✝) (↑(C σ R) a * f)
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
⊢ a • f = ↑(C σ R) a * f
ext
no goals
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
n✝ : σ →₀ ℕ
⊢ ↑(coeff R n✝) (a • f) = ↑(coeff R n✝) (↑(C σ R) a * f)
simp