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

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ weightedOrder w 0 = ⊤
Tactic:
rw [weightedOrder, dif_pos rfl]
State after:
no goals