Nonsingular inverses

In this file, we define an inverse for square matrices of invertible determinant.

For matrices that are not square or not of full rank, there is a more general notion of pseudoinverses which we do not consider here.

The definition of inverse used in this file is the adjugate divided by the determinant. We show that dividing the adjugate by det A (if possible), giving a matrix A⁻¹ (nonsing_inv), will result in a multiplicative inverse to A.

Note that there are at least three different inverses in mathlib:

• A⁻¹ (Inv.inv): alone, this satisfies no properties, although it is usually used in conjunction with Group or GroupWithZero. On matrices, this is defined to be zero when no inverse exists.
• ⅟A (invOf): this is only available in the presence of [Invertible A], which guarantees an inverse exists.
• Ring.inverse A: this is defined on any MonoidWithZero, and just like ⁻¹ on matrices, is defined to be zero when no inverse exists.

We start by working with Invertible, and show the main results:

• Matrix.invertibleOfDetInvertible
• Matrix.detInvertibleOfInvertible
• Matrix.isUnit_iff_isUnit_det
• Matrix.mul_eq_one_comm

After this we define Matrix.inv and show it matches ⅟A and Ring.inverse A. The rest of the results in the file are then about A⁻¹

References

• https://en.wikipedia.org/wiki/Cramer's_rule#Finding_inverse_matrix

Tags

matrix inverse, cramer, cramer's rule, adjugate

Matrices are Invertible iff their determinants are

def Matrix.invertibleOfDetInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A.det] : Invertible A

If A.det has a constructive inverse, produce one for A.

Equations

• A.invertibleOfDetInvertible = { invOf := ⅟A.det • A.adjugate, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem Matrix.invOf_eq {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A.det] [Invertible A] : ⅟A = ⅟A.det • A.adjugate

def Matrix.detInvertibleOfLeftInverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A B : Matrix n n α) (h : B * A = 1) : Invertible A.det

A.det is invertible if A has a left inverse.

Equations

• A.detInvertibleOfLeftInverse B h = { invOf := B.det, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

def Matrix.detInvertibleOfRightInverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A B : Matrix n n α) (h : A * B = 1) : Invertible A.det

A.det is invertible if A has a right inverse.

Equations

• A.detInvertibleOfRightInverse B h = { invOf := B.det, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

def Matrix.detInvertibleOfInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : Invertible A.det

If A has a constructive inverse, produce one for A.det.

Equations

• A.detInvertibleOfInvertible = A.detInvertibleOfLeftInverse ⅟A ⋯

theorem Matrix.det_invOf {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] [Invertible A.det] : (⅟A).det = ⅟A.det

def Matrix.invertibleEquivDetInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) : Invertible A ≃ Invertible A.det

Together Matrix.detInvertibleOfInvertible and Matrix.invertibleOfDetInvertible form an equivalence, although both sides of the equiv are subsingleton anyway.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.invertibleEquivDetInvertible_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : A.invertibleEquivDetInvertible inst✝ = A.detInvertibleOfInvertible

@[simp]

theorem Matrix.invertibleEquivDetInvertible_symm_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A.det] : A.invertibleEquivDetInvertible.symm inst✝ = A.invertibleOfDetInvertible

theorem Matrix.mul_eq_one_comm {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} : A * B = 1 ↔ B * A = 1

def Matrix.invertibleOfLeftInverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A B : Matrix n n α) (h : B * A = 1) : Invertible A

We can construct an instance of invertible A if A has a left inverse.

Equations

• A.invertibleOfLeftInverse B h = { invOf := B, invOf_mul_self := h, mul_invOf_self := ⋯ }

def Matrix.invertibleOfRightInverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A B : Matrix n n α) (h : A * B = 1) : Invertible A

We can construct an instance of invertible A if A has a right inverse.

Equations

• A.invertibleOfRightInverse B h = { invOf := B, invOf_mul_self := ⋯, mul_invOf_self := h }

def Matrix.unitOfDetInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A.det] : (Matrix n n α)ˣ

Given a proof that A.det has a constructive inverse, lift A to (Matrix n n α)ˣ

Equations

• A.unitOfDetInvertible = unitOfInvertible A

theorem Matrix.isUnit_iff_isUnit_det {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) : IsUnit A ↔ IsUnit A.det

When lowered to a prop, Matrix.invertibleEquivDetInvertible forms an iff.

@[simp]

theorem Matrix.isUnits_det_units {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : (Matrix n n α)ˣ) : IsUnit (↑A).det

Variants of the statements above with IsUnit

theorem Matrix.isUnit_det_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : IsUnit A.det

theorem Matrix.isUnit_of_left_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : B * A = 1) : IsUnit A

theorem Matrix.exists_left_inverse_iff_isUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} : (∃ (B : Matrix n n α), B * A = 1) ↔ IsUnit A

theorem Matrix.isUnit_of_right_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : A * B = 1) : IsUnit A

theorem Matrix.exists_right_inverse_iff_isUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} : (∃ (B : Matrix n n α), A * B = 1) ↔ IsUnit A

theorem Matrix.isUnit_det_of_left_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : B * A = 1) : IsUnit A.det

theorem Matrix.isUnit_det_of_right_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : A * B = 1) : IsUnit A.det

theorem Matrix.det_ne_zero_of_left_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} [Nontrivial α] (h : B * A = 1) : A.det ≠ 0

theorem Matrix.det_ne_zero_of_right_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} [Nontrivial α] (h : A * B = 1) : A.det ≠ 0

theorem Matrix.mul_eq_one_comm_of_equiv {m : Type u} {n : Type u'} {α : Type v} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m n α} {B : Matrix n m α} (e : m ≃ n) : A * B = 1 ↔ B * A = 1

A version of mul_eq_one_comm that works for square matrices with rectangular types.

theorem Matrix.isUnit_det_transpose {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : IsUnit A.transpose.det

A noncomputable Inv instance

noncomputable instance Matrix.inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] : Inv (Matrix n n α)

The inverse of a square matrix, when it is invertible (and zero otherwise).

Equations

• Matrix.inv = { inv := fun (A : Matrix n n α) => Ring.inverse A.det • A.adjugate }

theorem Matrix.inv_def {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) : A⁻¹ = Ring.inverse A.det • A.adjugate

theorem Matrix.nonsing_inv_apply_not_isUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : ¬IsUnit A.det) : A⁻¹ = 0

theorem Matrix.nonsing_inv_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : A⁻¹ = ↑h.unit⁻¹ • A.adjugate

@[simp]

theorem Matrix.invOf_eq_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : ⅟A = A⁻¹

The nonsingular inverse is the same as invOf when A is invertible.

@[simp]

theorem Matrix.coe_units_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (↑A)⁻¹

Coercing the result of Units.instInv is the same as coercing first and applying the nonsingular inverse.

theorem Matrix.nonsing_inv_eq_ring_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) : A⁻¹ = Ring.inverse A

The nonsingular inverse is the same as the general Ring.inverse.

theorem Matrix.transpose_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) : A⁻¹.transpose = A.transpose⁻¹

theorem Matrix.conjTranspose_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [StarRing α] : A⁻¹.conjTranspose = A.conjTranspose⁻¹

@[simp]

theorem Matrix.mul_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : A * A⁻¹ = 1

The nonsing_inv of A is a right inverse.

@[simp]

theorem Matrix.nonsing_inv_mul {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : A⁻¹ * A = 1

The nonsing_inv of A is a left inverse.

instance Matrix.instInvertibleInv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : Invertible A⁻¹

Equations

• A.instInvertibleInv = ⋯.mpr inferInstance

@[simp]

theorem Matrix.inv_inv_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : A⁻¹⁻¹ = A

@[simp]

theorem Matrix.mul_nonsing_inv_cancel_right {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix m n α) (h : IsUnit A.det) : B * A * A⁻¹ = B

@[simp]

theorem Matrix.mul_nonsing_inv_cancel_left {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n m α) (h : IsUnit A.det) : A * (A⁻¹ * B) = B

@[simp]

theorem Matrix.nonsing_inv_mul_cancel_right {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix m n α) (h : IsUnit A.det) : B * A⁻¹ * A = B

@[simp]

theorem Matrix.nonsing_inv_mul_cancel_left {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n m α) (h : IsUnit A.det) : A⁻¹ * (A * B) = B

@[simp]

theorem Matrix.mul_inv_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : A * A⁻¹ = 1

@[simp]

theorem Matrix.inv_mul_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : A⁻¹ * A = 1

@[simp]

theorem Matrix.mul_inv_cancel_right_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix m n α) [Invertible A] : B * A * A⁻¹ = B

@[simp]

theorem Matrix.mul_inv_cancel_left_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n m α) [Invertible A] : A * (A⁻¹ * B) = B

@[simp]

theorem Matrix.inv_mul_cancel_right_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix m n α) [Invertible A] : B * A⁻¹ * A = B

@[simp]

theorem Matrix.inv_mul_cancel_left_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n m α) [Invertible A] : A⁻¹ * (A * B) = B

theorem Matrix.inv_mul_eq_iff_eq_mul_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A B C : Matrix n n α) [Invertible A] : A⁻¹ * B = C ↔ B = A * C

theorem Matrix.mul_inv_eq_iff_eq_mul_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A B C : Matrix n n α) [Invertible A] : B * A⁻¹ = C ↔ B = C * A

theorem Matrix.inv_mulVec_eq_vec {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} [Invertible A] {u v : n → α} (hM : u = A.mulVec v) : A⁻¹.mulVec u = v

theorem Matrix.mul_right_injective_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : Function.Injective fun (x : Matrix n m α) => A * x

theorem Matrix.mul_left_injective_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] : Function.Injective fun (x : Matrix m n α) => x * A

theorem Matrix.mul_right_inj_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] {x y : Matrix n m α} : A * x = A * y ↔ x = y

theorem Matrix.mul_left_inj_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] {x y : Matrix m n α} : x * A = y * A ↔ x = y

theorem Matrix.mul_left_injective_of_inv {l : Type u_1} {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [Fintype m] [DecidableEq m] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) : Function.Injective fun (x : Matrix l m α) => x * A

theorem Matrix.mul_right_injective_of_inv {l : Type u_1} {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [Fintype m] [DecidableEq m] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) : Function.Injective fun (x : Matrix m l α) => B * x

theorem Matrix.vecMul_surjective_iff_exists_left_inverse {m : Type u} {n : Type u'} {R : Type u_2} [Semiring R] [DecidableEq n] [Fintype m] [Finite n] {A : Matrix m n R} : (Function.Surjective fun (v : m → R) => Matrix.vecMul v A) ↔ ∃ (B : Matrix n m R), B * A = 1

theorem Matrix.mulVec_surjective_iff_exists_right_inverse {m : Type u} {n : Type u'} {R : Type u_2} [Semiring R] [DecidableEq m] [Finite m] [Fintype n] {A : Matrix m n R} : Function.Surjective A.mulVec ↔ ∃ (B : Matrix n m R), A * B = 1

theorem Matrix.vecMul_surjective_iff_isUnit {m : Type u} [DecidableEq m] {R : Type u_2} [CommRing R] [Fintype m] {A : Matrix m m R} : (Function.Surjective fun (v : m → R) => Matrix.vecMul v A) ↔ IsUnit A

theorem Matrix.mulVec_surjective_iff_isUnit {m : Type u} [DecidableEq m] {R : Type u_2} [CommRing R] [Fintype m] {A : Matrix m m R} : Function.Surjective A.mulVec ↔ IsUnit A

theorem Matrix.vecMul_injective_iff_isUnit {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] {A : Matrix m m K} : (Function.Injective fun (v : m → K) => Matrix.vecMul v A) ↔ IsUnit A

theorem Matrix.mulVec_injective_iff_isUnit {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] {A : Matrix m m K} : Function.Injective A.mulVec ↔ IsUnit A

theorem Matrix.linearIndependent_rows_iff_isUnit {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] {A : Matrix m m K} : (LinearIndependent K fun (i : m) => A i) ↔ IsUnit A

theorem Matrix.linearIndependent_cols_iff_isUnit {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] {A : Matrix m m K} : (LinearIndependent K fun (i : m) => A.transpose i) ↔ IsUnit A

theorem Matrix.vecMul_surjective_of_invertible {m : Type u} [DecidableEq m] {R : Type u_2} [CommRing R] [Fintype m] (A : Matrix m m R) [Invertible A] : Function.Surjective fun (v : m → R) => Matrix.vecMul v A

theorem Matrix.mulVec_surjective_of_invertible {m : Type u} [DecidableEq m] {R : Type u_2} [CommRing R] [Fintype m] (A : Matrix m m R) [Invertible A] : Function.Surjective A.mulVec

theorem Matrix.vecMul_injective_of_invertible {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] (A : Matrix m m K) [Invertible A] : Function.Injective fun (v : m → K) => Matrix.vecMul v A

theorem Matrix.mulVec_injective_of_invertible {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] (A : Matrix m m K) [Invertible A] : Function.Injective A.mulVec

theorem Matrix.linearIndependent_rows_of_invertible {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] (A : Matrix m m K) [Invertible A] : LinearIndependent K fun (i : m) => A i

theorem Matrix.linearIndependent_cols_of_invertible {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] (A : Matrix m m K) [Invertible A] : LinearIndependent K fun (i : m) => A.transpose i

theorem Matrix.nonsing_inv_cancel_or_zero {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) : A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

theorem Matrix.det_nonsing_inv_mul_det {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : A⁻¹.det * A.det = 1

@[simp]

theorem Matrix.det_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) : A⁻¹.det = Ring.inverse A.det

theorem Matrix.isUnit_nonsing_inv_det {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : IsUnit A⁻¹.det

@[simp]

theorem Matrix.nonsing_inv_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : A⁻¹⁻¹ = A

theorem Matrix.isUnit_nonsing_inv_det_iff {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} : IsUnit A⁻¹.det ↔ IsUnit A.det

@[simp]

theorem Matrix.isUnit_nonsing_inv_iff {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} : IsUnit A⁻¹ ↔ IsUnit A

noncomputable def Matrix.invertibleOfIsUnitDet {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : Invertible A

A version of Matrix.invertibleOfDetInvertible with the inverse defeq to A⁻¹ that is therefore noncomputable.

Equations

• A.invertibleOfIsUnitDet h = { invOf := A⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

noncomputable def Matrix.nonsingInvUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : (Matrix n n α)ˣ

A version of Matrix.unitOfDetInvertible with the inverse defeq to A⁻¹ that is therefore noncomputable.

Equations

• A.nonsingInvUnit h = unitOfInvertible A

theorem Matrix.unitOfDetInvertible_eq_nonsingInvUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A.det] : A.unitOfDetInvertible = A.nonsingInvUnit ⋯

theorem Matrix.inv_eq_left_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : B * A = 1) : A⁻¹ = B

If matrix A is left invertible, then its inverse equals its left inverse.

theorem Matrix.inv_eq_right_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : A * B = 1) : A⁻¹ = B

If matrix A is right invertible, then its inverse equals its right inverse.

theorem Matrix.left_inv_eq_left_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B C : Matrix n n α} (h : B * A = 1) (g : C * A = 1) : B = C

The left inverse of matrix A is unique when existing.

theorem Matrix.right_inv_eq_right_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B C : Matrix n n α} (h : A * B = 1) (g : A * C = 1) : B = C

The right inverse of matrix A is unique when existing.

theorem Matrix.right_inv_eq_left_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B C : Matrix n n α} (h : A * B = 1) (g : C * A = 1) : B = C

The right inverse of matrix A equals the left inverse of A when they exist.

theorem Matrix.inv_inj {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B

@[simp]

theorem Matrix.inv_zero {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] : 0⁻¹ = 0

noncomputable instance Matrix.instInvOneClass {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] : InvOneClass (Matrix n n α)

Equations

• Matrix.instInvOneClass = InvOneClass.mk ⋯

theorem Matrix.inv_smul {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (k : α) [Invertible k] (h : IsUnit A.det) : (k • A)⁻¹ = ⅟k • A⁻¹

theorem Matrix.inv_smul' {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A⁻¹

theorem Matrix.inv_adjugate {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) : A.adjugate⁻¹ = h.unit⁻¹ • A

def Matrix.diagonalInvertible {n : Type u'} [Fintype n] [DecidableEq n] {α : Type u_2} [NonAssocSemiring α] (v : n → α) [Invertible v] : Invertible (Matrix.diagonal v)

diagonal v is invertible if v is

Equations

• Matrix.diagonalInvertible v = Invertible.map (Matrix.diagonalRingHom n α) v

theorem Matrix.invOf_diagonal_eq {n : Type u'} [Fintype n] [DecidableEq n] {α : Type u_2} [Semiring α] (v : n → α) [Invertible v] [Invertible (Matrix.diagonal v)] : ⅟(Matrix.diagonal v) = Matrix.diagonal ⅟v

def Matrix.invertibleOfDiagonalInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (v : n → α) [Invertible (Matrix.diagonal v)] : Invertible v

v is invertible if diagonal v is

Equations

• Matrix.invertibleOfDiagonalInvertible v = { invOf := (⅟(Matrix.diagonal v)).diag, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

def Matrix.diagonalInvertibleEquivInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (v : n → α) : Invertible (Matrix.diagonal v) ≃ Invertible v

Together Matrix.diagonalInvertible and Matrix.invertibleOfDiagonalInvertible form an equivalence, although both sides of the equiv are subsingleton anyway.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.diagonalInvertibleEquivInvertible_symm_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (v : n → α) [Invertible v] : (Matrix.diagonalInvertibleEquivInvertible v).symm inst✝ = Matrix.diagonalInvertible v

@[simp]

theorem Matrix.diagonalInvertibleEquivInvertible_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (v : n → α) [Invertible (Matrix.diagonal v)] : (Matrix.diagonalInvertibleEquivInvertible v) inst✝ = Matrix.invertibleOfDiagonalInvertible v

@[simp]

theorem Matrix.isUnit_diagonal {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {v : n → α} : IsUnit (Matrix.diagonal v) ↔ IsUnit v

When lowered to a prop, Matrix.diagonalInvertibleEquivInvertible forms an iff.

theorem Matrix.inv_diagonal {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (v : n → α) : (Matrix.diagonal v)⁻¹ = Matrix.diagonal (Ring.inverse v)

@[simp]

theorem Matrix.inv_subsingleton {m : Type u} {α : Type v} [CommRing α] [Subsingleton m] [Fintype m] [DecidableEq m] (A : Matrix m m α) : A⁻¹ = Matrix.diagonal fun (i : m) => Ring.inverse (A i i)

The inverse of a 1×1 or 0×0 matrix is always diagonal.

While we could write this as of fun _ _ => Ring.inverse (A default default) on the RHS, this is less useful because:

• It wouldn't work for 0×0 matrices.
• More things are true about diagonal matrices than constant matrices, and so more lemmas exist.

Matrix.diagonal_unique can be used to reach this form, while Ring.inverse_eq_inv can be used to replace Ring.inverse with ⁻¹.

theorem Matrix.add_mul_mul_inv_eq_sub {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) : (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

The Woodbury Identity (⁻¹ version).

@[simp]

theorem Matrix.inv_inv_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹

theorem Matrix.inv_add_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : IsUnit A ↔ IsUnit B) : A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹

The Matrix version of inv_add_inv'

theorem Matrix.inv_sub_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A B : Matrix n n α} (h : IsUnit A ↔ IsUnit B) : A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹

The Matrix version of inv_sub_inv'

theorem Matrix.mul_inv_rev {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A B : Matrix n n α) : (A * B)⁻¹ = B⁻¹ * A⁻¹

theorem Matrix.list_prod_inv_reverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (l : List (Matrix n n α)) : l.prod⁻¹ = (List.map Inv.inv l.reverse).prod

A version of List.prod_inv_reverse for Matrix.inv.

@[simp]

theorem Matrix.det_smul_inv_mulVec_eq_cramer {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹.mulVec b = A.cramer b

One form of Cramer's rule. See Matrix.mulVec_cramer for a stronger form.

@[simp]

theorem Matrix.det_smul_inv_vecMul_eq_cramer_transpose {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • Matrix.vecMul b A⁻¹ = A.transpose.cramer b

One form of Cramer's rule. See Matrix.mulVec_cramer for a stronger form.

Inverses of permutated matrices

Note that the simp-normal form of Matrix.reindex is Matrix.submatrix, so we prove most of these results about only the latter.

def Matrix.submatrixEquivInvertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] : Invertible (A.submatrix ⇑e₁ ⇑e₂)

A.submatrix e₁ e₂ is invertible if A is

Equations

• A.submatrixEquivInvertible e₁ e₂ = (A.submatrix ⇑e₁ ⇑e₂).invertibleOfRightInverse ((⅟A).submatrix ⇑e₂ ⇑e₁) ⋯

def Matrix.invertibleOfSubmatrixEquivInvertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible (A.submatrix ⇑e₁ ⇑e₂)] : Invertible A

A is invertible if A.submatrix e₁ e₂ is

Equations

• A.invertibleOfSubmatrixEquivInvertible e₁ e₂ = A.invertibleOfRightInverse ((⅟(A.submatrix ⇑e₁ ⇑e₂)).submatrix ⇑e₂.symm ⇑e₁.symm) ⋯

theorem Matrix.invOf_submatrix_equiv_eq {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] [Invertible (A.submatrix ⇑e₁ ⇑e₂)] : ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁

def Matrix.submatrixEquivInvertibleEquivInvertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) : Invertible (A.submatrix ⇑e₁ ⇑e₂) ≃ Invertible A

Together Matrix.submatrixEquivInvertible and Matrix.invertibleOfSubmatrixEquivInvertible form an equivalence, although both sides of the equiv are subsingleton anyway.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.submatrixEquivInvertibleEquivInvertible_symm_apply {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) (x✝ : Invertible A) : (A.submatrixEquivInvertibleEquivInvertible e₁ e₂).symm x✝ = A.submatrixEquivInvertible e₁ e₂

@[simp]

theorem Matrix.submatrixEquivInvertibleEquivInvertible_apply {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) (x✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)) : (A.submatrixEquivInvertibleEquivInvertible e₁ e₂) x✝ = A.invertibleOfSubmatrixEquivInvertible e₁ e₂

@[simp]

theorem Matrix.isUnit_submatrix_equiv {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] {A : Matrix m m α} (e₁ e₂ : n ≃ m) : IsUnit (A.submatrix ⇑e₁ ⇑e₂) ↔ IsUnit A

When lowered to a prop, Matrix.invertibleOfSubmatrixEquivInvertible forms an iff.

@[simp]

theorem Matrix.inv_submatrix_equiv {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) : (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁

theorem Matrix.inv_reindex {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (e₁ e₂ : n ≃ m) (A : Matrix n n α) : ((Matrix.reindex e₁ e₂) A)⁻¹ = (Matrix.reindex e₂ e₁) A⁻¹

More results about determinants

theorem Matrix.det_conj {m : Type u} {α : Type v} [CommRing α] [Fintype m] [DecidableEq m] {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : (M * N * M⁻¹).det = N.det

A variant of Matrix.det_units_conj.

theorem Matrix.det_conj' {m : Type u} {α : Type v} [CommRing α] [Fintype m] [DecidableEq m] {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : (M⁻¹ * N * M).det = N.det

A variant of Matrix.det_units_conj'.

More results about traces

theorem Matrix.trace_conj {m : Type u} {α : Type v} [CommRing α] [Fintype m] [DecidableEq m] {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : (M * N * M⁻¹).trace = N.trace

A variant of Matrix.trace_units_conj.

theorem Matrix.trace_conj' {m : Type u} {α : Type v} [CommRing α] [Fintype m] [DecidableEq m] {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : (M⁻¹ * N * M).trace = N.trace

A variant of Matrix.trace_units_conj'.