toIsOrderedAddMonoid — Mathlib

English

There is a default instance providing, for any x ≤ y, an element witnessing the difference in the form star(s)·s.

Русский

Существует стандартный экземпляр, который для каждого x ≤ y находит свидетельство разности в виде star(s)·s.

LaTeX

$$$\\\\exists s \\\\in R, \\\\ y = x + star(s) \\\\cdot s \\\\text{ whenever } x \\\\le y.$$$

Lean4

instance (priority := 100) toIsOrderedAddMonoid : IsOrderedAddMonoid R where
  add_le_add_left := fun x y hle z ↦ by
    rw [StarOrderedRing.le_iff] at hle ⊢
    refine hle.imp fun s hs ↦ ?_
    rw [hs.2, add_assoc]
    exact
      ⟨hs.1, rfl⟩
        -- see note [lower instance priority]

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