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

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
h : a ≠ 0
⊢ weightedOrder w ((monomial α d) a) = ↑((weight w) d)
Tactic:
classical
rw [weightedOrder_monomial, if_neg h]
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
a : α
h : a ≠ 0
⊢ weightedOrder w ((monomial α d) a) = ↑((weight w) d)
Tactic:
rw [weightedOrder_monomial, if_neg h]
State after:
no goals