isRegular — Mathlib

English

If R is a monoid, an element in Rˣ is regular.

Русский

Если R — моноид, элемент в Rˣ регулярен.

LaTeX

$$$ IsRegular (a : R) \text{ for } a \in Rˣ $$$

Lean4

/-- If `R` is a monoid, an element in `Rˣ` is regular. -/
@[to_additive /-- If `R` is an additive monoid, an element in `add_units R` is add-regular. -/
    ]
theorem isRegular (a : Rˣ) : IsRegular (a : R) :=
  ⟨isLeftRegular_of_mul_eq_one a.inv_mul, isRightRegular_of_mul_eq_one a.mul_inv⟩

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