Theorems · Theorem · linear algebra

Matrix.left_inv_eq_left_inv

∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B C : Matrix n n α},
  B * A = 1 → C * A = 1 → B = C

The left inverse of matrix A is unique when existing.

Defined in

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Cited by

1 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqCommRing