isRightRegular_of_mul_eq_one — Mathlib

English

If a * b = 1, then a is right-regular.

Русский

Если a * b = 1, тогда a является правой регулярностью.

LaTeX

$$$ a * b = 1 \rightarrow IsRightRegular a $$$

Lean4

/-- An element admitting a right inverse is right-regular. -/
@[to_additive /-- An element admitting a right additive opposite is add-right-regular. -/
    ]
theorem isRightRegular_of_mul_eq_one (h : a * b = 1) : IsRightRegular a :=
  IsRightRegular.of_mul (a := b) (by rw [h]; exact isRegular_one.right)

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