Theorem: MvPowerSeries.exists_coeff_ne_zero_iff_ne_zero (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
f : MvPowerSeries σ α
⊢ (∃ d, (coeff α d) f ≠ 0) ↔ f ≠ 0
Tactic:
simp only [ext_iff, ne_eq, coeff_zero, not_forall]
State after:
no goals