# mathlib3documentation

linear_algebra.matrix.nonsingular_inverse

# Nonsingular inverses #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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⁻¹ (has_inv.inv): alone, this satisfies no properties, although it is usually used in conjunction with group or group_with_zero. On matrices, this is defined to be zero when no inverse exists.
• ⅟A (inv_of): this is only available in the presence of [invertible A], which guarantees an inverse exists.
• ring.inverse A: this is defined on any monoid_with_zero, 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.invertible_of_det_invertible
• matrix.det_invertible_of_invertible
• matrix.is_unit_iff_is_unit_det
• matrix.mul_eq_one_comm

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

## Tags #

matrix inverse, cramer, cramer's rule, adjugate

### Matrices are invertible iff their determinants are #

def matrix.invertible_of_det_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A.det] :

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

Equations
theorem matrix.inv_of_eq {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A.det] [invertible A] :
def matrix.det_invertible_of_left_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A B : n α) (h : B.mul A = 1) :

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

Equations
def matrix.det_invertible_of_right_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A B : n α) (h : A.mul B = 1) :

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

Equations
def matrix.det_invertible_of_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :

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

Equations
theorem matrix.det_inv_of {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] [invertible A.det] :
( A).det = A.det
@[simp]
theorem matrix.invertible_equiv_det_invertible_apply {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :
@[simp]
theorem matrix.invertible_equiv_det_invertible_symm_apply {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A.det] :
def matrix.invertible_equiv_det_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) :

Together matrix.det_invertible_of_invertible and matrix.invertible_of_det_invertible form an equivalence, although both sides of the equiv are subsingleton anyway.

Equations
theorem matrix.mul_eq_one_comm {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : n α} :
A.mul B = 1 B.mul A = 1
def matrix.invertible_of_left_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A B : n α) (h : B.mul A = 1) :

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

Equations
def matrix.invertible_of_right_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A B : n α) (h : A.mul B = 1) :

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

Equations
@[protected, instance]
def matrix.invertible_transpose {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :

The transpose of an invertible matrix is invertible.

Equations
def matrix.invertible__of_invertible_transpose {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α)  :

A matrix is invertible if the transpose is invertible.

Equations
def matrix.invertible_of_invertible_conj_transpose {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [star_ring α]  :

A matrix is invertible if the conjugate transpose is invertible.

Equations
def matrix.unit_of_det_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A.det] :
(matrix n n α)ˣ

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

Equations
theorem matrix.is_unit_iff_is_unit_det {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) :

When lowered to a prop, matrix.invertible_equiv_det_invertible forms an iff.

#### Variants of the statements above with is_unit#

theorem matrix.is_unit_det_of_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :
theorem matrix.is_unit_of_left_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : n α} (h : B.mul A = 1) :
theorem matrix.is_unit_of_right_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : n α} (h : A.mul B = 1) :
theorem matrix.is_unit_det_of_left_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : n α} (h : B.mul A = 1) :
theorem matrix.is_unit_det_of_right_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : n α} (h : A.mul B = 1) :
theorem matrix.det_ne_zero_of_left_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : n α} [nontrivial α] (h : B.mul A = 1) :
A.det 0
theorem matrix.det_ne_zero_of_right_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : n α} [nontrivial α] (h : A.mul B = 1) :
A.det 0
theorem matrix.is_unit_det_transpose {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :

### A noncomputable has_inv instance #

@[protected, instance]
noncomputable def matrix.has_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] :
has_inv (matrix n n α)

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

Equations
theorem matrix.inv_def {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) :
theorem matrix.nonsing_inv_apply_not_is_unit {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : ¬) :
A⁻¹ = 0
theorem matrix.nonsing_inv_apply {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :
@[simp]
theorem matrix.inv_of_eq_nonsing_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :

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

@[simp, norm_cast]
theorem matrix.coe_units_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : (matrix n n α)ˣ) :

Coercing the result of units.has_inv 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] [decidable_eq n] [comm_ring α] (A : n α) :

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

theorem matrix.transpose_nonsing_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) :
theorem matrix.conj_transpose_nonsing_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [star_ring α] :
@[simp]
theorem matrix.mul_nonsing_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :
A.mul A⁻¹ = 1

The nonsing_inv of A is a right inverse.

@[simp]
theorem matrix.nonsing_inv_mul {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :
A⁻¹.mul A = 1

The nonsing_inv of A is a left inverse.

@[protected, instance]
def matrix.has_inv.inv.invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :
Equations
@[simp]
theorem matrix.inv_inv_of_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :
@[simp]
theorem matrix.mul_nonsing_inv_cancel_right {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (B : n α) (h : is_unit A.det) :
(B.mul A).mul A⁻¹ = B
@[simp]
theorem matrix.mul_nonsing_inv_cancel_left {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (B : m α) (h : is_unit A.det) :
A.mul (A⁻¹.mul B) = B
@[simp]
theorem matrix.nonsing_inv_mul_cancel_right {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (B : n α) (h : is_unit A.det) :
(B.mul A⁻¹).mul A = B
@[simp]
theorem matrix.nonsing_inv_mul_cancel_left {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (B : m α) (h : is_unit A.det) :
A⁻¹.mul (A.mul B) = B
@[simp]
theorem matrix.mul_inv_of_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :
A.mul A⁻¹ = 1
@[simp]
theorem matrix.inv_mul_of_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) [invertible A] :
A⁻¹.mul A = 1
@[simp]
theorem matrix.mul_inv_cancel_right_of_invertible {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (B : n α) [invertible A] :
(B.mul A).mul A⁻¹ = B
@[simp]
theorem matrix.mul_inv_cancel_left_of_invertible {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (B : m α) [invertible A] :
A.mul (A⁻¹.mul B) = B
@[simp]
theorem matrix.inv_mul_cancel_right_of_invertible {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (B : n α) [invertible A] :
(B.mul A⁻¹).mul A = B
@[simp]
theorem matrix.inv_mul_cancel_left_of_invertible {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (B : m α) [invertible A] :
A⁻¹.mul (A.mul B) = B
theorem matrix.inv_mul_eq_iff_eq_mul_of_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A B C : n α) [invertible A] :
A⁻¹.mul B = C B = A.mul C
theorem matrix.mul_inv_eq_iff_eq_mul_of_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A B C : n α) [invertible A] :
B.mul A⁻¹ = C B = C.mul A
theorem matrix.nonsing_inv_cancel_or_zero {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) :
A⁻¹.mul A = 1 A.mul A⁻¹ = 1 A⁻¹ = 0
theorem matrix.det_nonsing_inv_mul_det {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :
A⁻¹.det * A.det = 1
@[simp]
theorem matrix.det_nonsing_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) :
theorem matrix.is_unit_nonsing_inv_det {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :
@[simp]
theorem matrix.nonsing_inv_nonsing_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :
theorem matrix.is_unit_nonsing_inv_det_iff {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A : n α} :
noncomputable def matrix.invertible_of_is_unit_det {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :

A version of matrix.invertible_of_det_invertible with the inverse defeq to A⁻¹ that is therefore noncomputable.

Equations
noncomputable def matrix.nonsing_inv_unit {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :
(matrix n n α)ˣ

A version of matrix.units_of_det_invertible with the inverse defeq to A⁻¹ that is therefore noncomputable.

Equations
theorem matrix.inv_eq_left_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : n α} (h : B.mul 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] [decidable_eq n] [comm_ring α] {A B : n α} (h : A.mul 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] [decidable_eq n] [comm_ring α] {A B C : n α} (h : B.mul A = 1) (g : C.mul 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] [decidable_eq n] [comm_ring α] {A B C : n α} (h : A.mul B = 1) (g : A.mul 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] [decidable_eq n] [comm_ring α] {A B C : n α} (h : A.mul B = 1) (g : C.mul 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] [decidable_eq n] [comm_ring α] {A B : n α} (h : A⁻¹ = B⁻¹) (h' : is_unit A.det) :
A = B
@[simp]
theorem matrix.inv_zero {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] :
0⁻¹ = 0
@[protected, instance]
noncomputable def matrix.inv_one_class {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] :
Equations
theorem matrix.inv_smul {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (k : α) [invertible k] (h : is_unit A.det) :
theorem matrix.inv_smul' {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (k : αˣ) (h : is_unit A.det) :
theorem matrix.inv_adjugate {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (h : is_unit A.det) :
def matrix.diagonal_invertible {n : Type u'} [fintype n] [decidable_eq n] {α : Type u_1} (v : n α) [invertible v] :

diagonal v is invertible if v is

Equations
theorem matrix.inv_of_diagonal_eq {n : Type u'} [fintype n] [decidable_eq n] {α : Type u_1} [semiring α] (v : n α) [invertible v]  :
def matrix.invertible_of_diagonal_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (v : n α)  :

v is invertible if diagonal v is

Equations
@[simp]
@[simp]
theorem matrix.diagonal_invertible_equiv_invertible_apply {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (v : n α)  :
def matrix.diagonal_invertible_equiv_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (v : n α) :

Together matrix.diagonal_invertible and matrix.invertible_of_diagonal_invertible form an equivalence, although both sides of the equiv are subsingleton anyway.

Equations
@[simp]
theorem matrix.is_unit_diagonal {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {v : n α} :

When lowered to a prop, matrix.diagonal_invertible_equiv_invertible forms an iff.

theorem matrix.inv_diagonal {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (v : n α) :
@[simp]
theorem matrix.inv_inv_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) :
theorem matrix.mul_inv_rev {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A B : n α) :
theorem matrix.list_prod_inv_reverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (l : list (matrix n n α)) :

A version of list.prod_inv_reverse for matrix.has_inv.

@[simp]
theorem matrix.det_smul_inv_mul_vec_eq_cramer {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (b : n α) (h : is_unit A.det) :

One form of Cramer's rule. See matrix.mul_vec_cramer for a stronger form.

@[simp]
theorem matrix.det_smul_inv_vec_mul_eq_cramer_transpose {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : n α) (b : n α) (h : is_unit A.det) :

One form of Cramer's rule. See matrix.mul_vec_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.submatrix_equiv_invertible {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] (A : m α) (e₁ e₂ : n m) [invertible A] :

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

Equations
def matrix.invertible_of_submatrix_equiv_invertible {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] (A : m α) (e₁ e₂ : n m) [invertible (A.submatrix e₁ e₂)] :

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

Equations
theorem matrix.inv_of_submatrix_equiv_eq {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] (A : m α) (e₁ e₂ : n m) [invertible A] [invertible (A.submatrix e₁ e₂)] :
(A.submatrix e₁ e₂) = ( A).submatrix e₂ e₁
def matrix.submatrix_equiv_invertible_equiv_invertible {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] (A : m α) (e₁ e₂ : n m) :

Together matrix.submatrix_equiv_invertible and matrix.invertible_of_submatrix_equiv_invertible form an equivalence, although both sides of the equiv are subsingleton anyway.

Equations
@[simp]
theorem matrix.submatrix_equiv_invertible_equiv_invertible_apply {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] (A : m α) (e₁ e₂ : n m) (_x : invertible (A.submatrix e₁ e₂)) :
@[simp]
theorem matrix.submatrix_equiv_invertible_equiv_invertible_symm_apply {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] (A : m α) (e₁ e₂ : n m) (_x : invertible A) :
.symm) _x = e₂
@[simp]
theorem matrix.is_unit_submatrix_equiv {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] {A : m α} (e₁ e₂ : n m) :
is_unit (A.submatrix e₁ e₂)

When lowered to a prop, matrix.invertible_of_submatrix_equiv_invertible forms an iff.

@[simp]
theorem matrix.inv_submatrix_equiv {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] (A : 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] [decidable_eq n] [comm_ring α] [fintype m] [decidable_eq m] (e₁ e₂ : n m) (A : n α) :
( e₂) A)⁻¹ = e₁) A⁻¹

### More results about determinants #

theorem matrix.det_conj {m : Type u} {α : Type v} [comm_ring α] [fintype m] [decidable_eq m] {M : m α} (h : is_unit M) (N : m α) :
((M.mul N).mul M⁻¹).det = N.det

A variant of matrix.det_units_conj.

theorem matrix.det_conj' {m : Type u} {α : Type v} [comm_ring α] [fintype m] [decidable_eq m] {M : m α} (h : is_unit M) (N : m α) :
((M⁻¹.mul N).mul M).det = N.det

A variant of matrix.det_units_conj'.