weightedOrder_monomial — Mathlib

English

The weighted order of the monomial a X^d is the weight of d, or ∞ if a = 0.

Русский

Весовой порядок мономиала a X^d равен weight_w(d) при a ≠ 0, и бесконечность, если a = 0.

LaTeX

$$weightedOrder w (monomial d a) = if a = 0 then ⊤ else weight w d$$

Lean4

/-- The weighted_order of the monomial `a*X^d` is infinite if `a = 0` and `weight w d` otherwise. -/
theorem weightedOrder_monomial {d : σ →₀ ℕ} {a : R} [Decidable (a = 0)] :
    weightedOrder w (monomial d a) = if a = 0 then (⊤ : ℕ∞) else weight w d := by
  classical
  split_ifs with h
  · rw [h, weightedOrder_eq_top_iff, LinearMap.map_zero]
  · rw [weightedOrder_eq_nat]
    constructor
    · use d
      simp only [coeff_monomial_same, ne_eq, h, not_false_eq_true, and_self]
    · intro b hb
      rw [coeff_monomial, if_neg]
      rintro rfl
      exact hb.false

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