instIsOrderedCancelAddMonoidDegLexNat

English

DegLex(α →₀ ℕ) forms an ordered cancel additive monoid, i.e., addition respects order and has cancellation on the left.

Русский

DegLex(α →₀ ℕ) образует упорядоченный моноид с отменой слева: сложение сохраняет порядок и удовлетворяет отмене слева.

LaTeX

$$$\text{IsOrderedCancelAddMonoid}\left(\DegLex(\alpha \to\_0 \mathbb{N})\right)$$$

Lean4

instance : IsOrderedCancelAddMonoid (DegLex (α →₀ ℕ))
    where
  le_of_add_le_add_left a b c
    h := by
    rw [le_iff] at h ⊢
    simpa only [ofDegLex_add, degree_add, add_lt_add_iff_left, add_right_inj, toLex_add, add_le_add_iff_left] using h
  add_le_add_left a b h
    c := by
    rw [le_iff] at h ⊢
    simpa [ofDegLex_add, degree_add] using h

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