left_inv_eq_left_inv — Mathlib

English

If B and C are left inverses of A, then B = C; i.e., left inverse is unique when it exists.

Русский

Если B и C — левый обратный к A, то B = C; левый обратный существует единственный.

LaTeX

$$If B A = 1 and C A = 1, then B = C.$$

Lean4

/-- The left inverse of matrix A is unique when existing. -/
theorem left_inv_eq_left_inv (h : B * A = 1) (g : C * A = 1) : B = C := by rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]

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