invertibleOfLeftInverse — Mathlib

English

If B is a left inverse of A, i.e., B · A = I, then A is invertible and B is its inverse.

Русский

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

LaTeX

$$$\text{If } B A = 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 left inverse. -/
def invertibleOfLeftInverse (h : B * A = 1) : Invertible A :=
  ⟨B, h, mul_eq_one_comm.mp h⟩

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