instIsOrderedCancelAddMonoidLexFinsupp

English

The lexicographic order on σ →₀ ℕ defines a MonomialOrder via the Lex order on σ →₀ ℕ.

Русский

Лексикографический порядок на σ →₀ ℕ задаёт порядок мономов через порядок Lex на σ →₀ ℕ.

LaTeX

$$$$ \\text{lex} : \\text{MonomialOrder } σ, \\quad \\text{syn} := \\text{Lex}(σ \\to_0 \\mathbb{N}). $$$$

Lean4

noncomputable instance {α N : Type*} [LinearOrder α] [AddCommMonoid N] [PartialOrder N] [IsOrderedCancelAddMonoid N] :
    IsOrderedCancelAddMonoid (Lex (α →₀ N))
    where
  le_of_add_le_add_left a b c h := by simpa only [add_le_add_iff_left] using h
  add_le_add_left a b h c := by simpa only [add_le_add_iff_left] using h

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