nonempty_invertible_iff_isUnit — Mathlib

English

Let α be a monoid and a ∈ α. Then a is a unit if and only if there exists x ∈ α such that a x = x a = 1. Equivalently, a has a two-sided inverse.

Русский

Пусть α — моноид и a ∈ α. Тогда a является единицей тогда и только тогда, когда существует x ∈ α такое, что a x = x a = 1. Эквивалентно: a имеет двусторонний обратный элемент.

LaTeX

$$$\mathrm{IsUnit}(a) \iff \exists b \in \alpha,\ a b = 1 \land b a = 1$$$

Lean4

@[simp]
theorem nonempty_invertible_iff_isUnit [Monoid α] (a : α) : Nonempty (Invertible a) ↔ IsUnit a :=
  ⟨Nonempty.rec <| @isUnit_of_invertible _ _ _, IsUnit.nonempty_invertible⟩

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