case h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ 1 ≠ 0
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ order (X ^ n) = ↑n
rw [X_pow_eq, order_monomial_of_ne_zero]
no goals
case h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ 1 ≠ 0
exact one_ne_zero