order_monomial_of_ne_zero — Mathlib

English

If the coefficient a is nonzero, the order of the monomial a*X^d is exactly degree(d).

Русский

Если коэффициент a не равен нулю, то порядок монома a·X^d равен степени d.

LaTeX

$$$ a \neq 0 \Rightarrow \operatorname{order}(\mathrm{monomial}(d,a)) = \operatorname{degree} d $$$

Lean4

/-- The order of the monomial `a*X^n` is `n` if `a ≠ 0`. -/
theorem order_monomial_of_ne_zero {d : σ →₀ ℕ} {a : R} (h : a ≠ 0) : order (monomial d a) = degree d :=
  by
  rw [degree_eq_weight_one]
  exact weightedOrder_monomial_of_ne_zero _ h

Похожие утверждения