invertible — Mathlib

English

From IsUnit a, one obtains an Invertible a, i.e., a has a two-sided inverse.

Русский

Из IsUnit a следует существование Invertible a, то есть у a есть двусторонний обратный элемент.

LaTeX

$$$ IsUnit(a) \Rightarrow Invertible(a)$$$

Lean4

/-- Convert `IsUnit` to `Invertible` using `Classical.choice`.

Prefer `casesI h.nonempty_invertible` over `letI := h.invertible` if you want to avoid choice. -/
noncomputable def invertible [Monoid α] {a : α} (h : IsUnit a) : Invertible a :=
  Classical.choice h.nonempty_invertible

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