toCanonicallyOrderedAdd — Mathlib

English

If α is an IdemSemiring, then its additive structure carries the canonical order, making α a canonically ordered additive monoid.

Русский

Если α — IdemSemiring, то его аддитивная структура получает канонически упорядоченный вид, превращая α в канонически упорядоченную аддитивную моноиду.

LaTeX

$$$\alpha \;\text{is canonically ordered under addition}$$$

Lean4

instance (priority := 100) toCanonicallyOrderedAdd : CanonicallyOrderedAdd α
    where
  exists_add_of_le h := ⟨_, h.add_eq_right.symm⟩
  le_add_self a b := add_eq_left_iff_le.1 <| by rw [add_assoc, add_idem]
  le_self_add a
    b :=
    add_eq_right_iff_le.1 <| by
      rw [← add_assoc, add_idem]
        -- See note [lower instance priority]

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