isUnit_iff_exists_inv — Mathlib

English

In a commutative monoid, IsUnit a is equivalent to the existence of b with a·b = 1.

Русский

В коммутативном моноиде IsUnit a эквивалентно существованию b такого, что a·b = 1.

LaTeX

$$IsUnit(a) \iff \exists b, a \cdot b = 1$$

Lean4

@[to_additive]
theorem isUnit_iff_exists_inv [CommMonoid M] {a : M} : IsUnit a ↔ ∃ b, a * b = 1 :=
  ⟨fun h => h.exists_right_inv, fun ⟨b, hab⟩ => isUnit_of_mul_eq_one _ b hab⟩

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