Theorem: MvPowerSeries.coeff_truncFun' (DividedPowers/ForMathlib/RingTheory/MvPowerSeries/Trunc.lean)

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun' n φ) = if m ≤ n then (coeff R m) φ else 0
Tactic:
classical
simp [truncFun', MvPolynomial.coeff_sum]
State after:
no goals

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m (truncFun' n φ) = if m ≤ n then (coeff R m) φ else 0
Tactic:
simp [truncFun', MvPolynomial.coeff_sum]
State after:
no goals