invertibleOfRightInverse — Mathlib

English

If A has a right inverse B, i.e., A · B = I, then A is invertible with B as the inverse.

Русский

Если у A есть правой обратной B, то есть A·B = I, то A обратима и B — её обратная.

LaTeX

$$$\text{If } A B = I, \text{ then } A \text{ is invertible and } B \text{ is its inverse.}$$$

Lean4

/-- We can construct an instance of invertible A if A has a right inverse. -/
def invertibleOfRightInverse (h : A * B = 1) : Invertible A :=
  ⟨B, mul_eq_one_comm.mp h, h⟩

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