Theorem: MvPowerSeries.StronglySummable.order_tendsto_top_iff (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : Finite σ
f : ι → MvPowerSeries σ α
⊢ σ → 1 ≠ 0
Tactic:
simp
State after:
no goals