instCanonicallyOrderedAdd — Mathlib

English

The additive structure on FractionalIdeal S P is canonically ordered.

Русский

Аддитивная структура дробных идеалов S P упорядочена канонически.

LaTeX

$$$\mathrm{CanonicallyOrderedAdd}(\mathrm{FractionalIdeal}(S,P))$$$

Lean4

instance : CanonicallyOrderedAdd (FractionalIdeal S P)
    where
  exists_add_of_le h := ⟨_, (sup_eq_right.mpr h).symm⟩
  le_add_self _ _ := le_sup_right
  le_self_add _ _ := le_sup_left

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