order_monomial — Mathlib

English

If a ≠ 0, then the order of the monomial a X^n is exactly n.

Русский

Если a ≠ 0, то порядок монома a X^n равен точно n.

LaTeX

$$$\operatorname{order}(\mathrm{monomial}(n,a)) = n \quad \text{when } a \neq 0$$$

Lean4

/-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise. -/
theorem order_monomial (n : ℕ) (a : R) [Decidable (a = 0)] : order (monomial n a) = if a = 0 then (⊤ : ℕ∞) else n :=
  by
  split_ifs with h
  · rw [h, order_eq_top, LinearMap.map_zero]
  · rw [order_eq]
    constructor <;> intro i hi
    · simp only [Nat.cast_inj] at hi
      rwa [hi, coeff_monomial_same]
    · simp only [Nat.cast_lt] at hi
      rw [coeff_monomial, if_neg]
      exact ne_of_lt hi

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