isRegular_one — Mathlib

English

In any monoid, the element 1 is regular.

Русский

В любом моноиде элемент 1 является регулярным.

LaTeX

$$$ IsRegular (1 : R) $$$

Lean4

/-- If multiplying by `1` on either side is the identity, `1` is regular. -/
@[to_additive /-- If adding `0` on either side is the identity, `0` is regular. -/
    ]
theorem isRegular_one : IsRegular (1 : R) :=
  ⟨fun a b ab => (one_mul a).symm.trans (Eq.trans ab (one_mul b)), fun a b ab =>
    (mul_one a).symm.trans (Eq.trans ab (mul_one b))⟩

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