order_monomial — Mathlib

English

The order of the monomial a*X^d is infinite if a = 0, and equals the degree of d otherwise.

Русский

Порядок монома a·X^d бесконечен, если a = 0, иначе равен степени d.

LaTeX

$$$ \operatorname{order}(\mathrm{monomial}(d,a)) = \begin{cases} \top, & a = 0, \\ \uparrow (\operatorname{degree} d), & a \neq 0. \end{cases} $$$

Lean4

/-- The order of the monomial `a*X^d` is infinite if `a = 0` and `degree d` otherwise. -/
theorem order_monomial {d : σ →₀ ℕ} {a : R} [Decidable (a = 0)] :
    order (monomial d a) = if a = 0 then (⊤ : ℕ∞) else ↑(degree d) :=
  by
  rw [degree_eq_weight_one]
  exact weightedOrder_monomial _

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