exists_left_inverse_iff_isUnit — Mathlib

English

There exists a left inverse of A if and only if A is a unit.

Русский

Существует левый обратный к A тогда и только тогда, когда A единица (обратима).

LaTeX

$$$\exists B: BA = I \quad\Longleftrightarrow\quad A \text{ is a unit}$$$

Lean4

theorem exists_left_inverse_iff_isUnit : (∃ B, B * A = 1) ↔ IsUnit A :=
  ⟨fun ⟨_, h⟩ ↦ isUnit_of_left_inverse h, fun h ↦
    have := h.invertible;
    ⟨⅟A, invOf_mul_self' A⟩⟩

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