# 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} [] [] [] (A : Matrix n n α) [] :

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

Equations
• = { invOf := , invOf_mul_self := , mul_invOf_self := }
Instances For
theorem Matrix.invOf_eq {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] [] :
A =
def Matrix.detInvertibleOfLeftInverse {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n n α) (h : B * A = 1) :

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

Equations
• = { invOf := , invOf_mul_self := , mul_invOf_self := }
Instances For
def Matrix.detInvertibleOfRightInverse {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n n α) (h : A * B = 1) :

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

Equations
• = { invOf := , invOf_mul_self := , mul_invOf_self := }
Instances For
def Matrix.detInvertibleOfInvertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :

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

Equations
Instances For
theorem Matrix.det_invOf {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] [] :
= ()
@[simp]
theorem Matrix.invertibleEquivDetInvertible_symm_apply {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
.symm inst✝ =
@[simp]
theorem Matrix.invertibleEquivDetInvertible_apply {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
def Matrix.invertibleEquivDetInvertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) :

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.
Instances For
theorem Matrix.mul_eq_one_comm {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} {B : Matrix n n α} :
A * B = 1 B * A = 1
def Matrix.invertibleOfLeftInverse {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n n α) (h : B * A = 1) :

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

Equations
• = { invOf := B, invOf_mul_self := h, mul_invOf_self := }
Instances For
def Matrix.invertibleOfRightInverse {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n n α) (h : A * B = 1) :

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

Equations
• = { invOf := B, invOf_mul_self := , mul_invOf_self := h }
Instances For
def Matrix.unitOfDetInvertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
(Matrix n n α)ˣ

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

Equations
Instances For
theorem Matrix.isUnit_iff_isUnit_det {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) :

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

#### Variants of the statements above with IsUnit#

theorem Matrix.isUnit_det_of_invertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
theorem Matrix.isUnit_of_left_inverse {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} {B : Matrix n n α} (h : B * A = 1) :
theorem Matrix.exists_left_inverse_iff_isUnit {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} :
(∃ (B : Matrix n n α), B * A = 1)
theorem Matrix.isUnit_of_right_inverse {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} {B : Matrix n n α} (h : A * B = 1) :
theorem Matrix.exists_right_inverse_iff_isUnit {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} :
(∃ (B : Matrix n n α), A * B = 1)
theorem Matrix.isUnit_det_of_left_inverse {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} {B : Matrix n n α} (h : B * A = 1) :
theorem Matrix.isUnit_det_of_right_inverse {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} {B : Matrix n n α} (h : A * B = 1) :
theorem Matrix.det_ne_zero_of_left_inverse {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} {B : Matrix n n α} [] (h : B * A = 1) :
0
theorem Matrix.det_ne_zero_of_right_inverse {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} {B : Matrix n n α} [] (h : A * B = 1) :
0
theorem Matrix.isUnit_det_transpose {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :

### A noncomputable Inv instance #

noncomputable instance Matrix.inv {n : Type u'} {α : Type v} [] [] [] :
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 α) => }
theorem Matrix.inv_def {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) :
theorem Matrix.nonsing_inv_apply_not_isUnit {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : ¬IsUnit ()) :
A⁻¹ = 0
theorem Matrix.nonsing_inv_apply {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :
@[simp]
theorem Matrix.invOf_eq_nonsing_inv {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :

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

@[simp]
theorem Matrix.coe_units_inv {n : Type u'} {α : Type v} [] [] [] (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} [] [] [] (A : Matrix n n α) :

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

theorem Matrix.transpose_nonsing_inv {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) :
theorem Matrix.conjTranspose_nonsing_inv {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
@[simp]
theorem Matrix.mul_nonsing_inv {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :
A * A⁻¹ = 1

The nonsing_inv of A is a right inverse.

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

The nonsing_inv of A is a left inverse.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Matrix.inv_inv_of_invertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
@[simp]
theorem Matrix.mul_nonsing_inv_cancel_right {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix m n α) (h : IsUnit ()) :
B * A * A⁻¹ = B
@[simp]
theorem Matrix.mul_nonsing_inv_cancel_left {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n m α) (h : IsUnit ()) :
A * (A⁻¹ * B) = B
@[simp]
theorem Matrix.nonsing_inv_mul_cancel_right {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix m n α) (h : IsUnit ()) :
B * A⁻¹ * A = B
@[simp]
theorem Matrix.nonsing_inv_mul_cancel_left {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n m α) (h : IsUnit ()) :
A⁻¹ * (A * B) = B
@[simp]
theorem Matrix.mul_inv_of_invertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
A * A⁻¹ = 1
@[simp]
theorem Matrix.inv_mul_of_invertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
A⁻¹ * A = 1
@[simp]
theorem Matrix.mul_inv_cancel_right_of_invertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix m n α) [] :
B * A * A⁻¹ = B
@[simp]
theorem Matrix.mul_inv_cancel_left_of_invertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n m α) [] :
A * (A⁻¹ * B) = B
@[simp]
theorem Matrix.inv_mul_cancel_right_of_invertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix m n α) [] :
B * A⁻¹ * A = B
@[simp]
theorem Matrix.inv_mul_cancel_left_of_invertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n m α) [] :
A⁻¹ * (A * B) = B
theorem Matrix.inv_mul_eq_iff_eq_mul_of_invertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n n α) (C : Matrix n n α) [] :
A⁻¹ * B = C B = A * C
theorem Matrix.mul_inv_eq_iff_eq_mul_of_invertible {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n n α) (C : Matrix n n α) [] :
B * A⁻¹ = C B = C * A
theorem Matrix.mul_right_injective_of_invertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
Function.Injective fun (x : Matrix n m α) => A * x
theorem Matrix.mul_left_injective_of_invertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
Function.Injective fun (x : Matrix m n α) => x * A
theorem Matrix.mul_right_inj_of_invertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] {x : Matrix n m α} {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} [] [] [] (A : Matrix n n α) [] {x : Matrix m n α} {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} [] [] [] [] (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} [] [] [] [] (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} [] [] [] {A : Matrix m n R} :
(Function.Surjective fun (v : mR) => ) ∃ (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} [] [] [] {A : Matrix m n R} :
∃ (B : Matrix n m R), A * B = 1
theorem Matrix.vecMul_surjective_iff_isUnit {m : Type u} [] {R : Type u_2} [] [] {A : Matrix m m R} :
(Function.Surjective fun (v : mR) => )
theorem Matrix.mulVec_surjective_iff_isUnit {m : Type u} [] {R : Type u_2} [] [] {A : Matrix m m R} :
theorem Matrix.vecMul_injective_iff_isUnit {m : Type u} [] {K : Type u_3} [] [] {A : Matrix m m K} :
(Function.Injective fun (v : mK) => )
theorem Matrix.mulVec_injective_iff_isUnit {m : Type u} [] {K : Type u_3} [] [] {A : Matrix m m K} :
theorem Matrix.linearIndependent_rows_iff_isUnit {m : Type u} [] {K : Type u_3} [] [] {A : Matrix m m K} :
(LinearIndependent K fun (i : m) => A i)
theorem Matrix.linearIndependent_cols_iff_isUnit {m : Type u} [] {K : Type u_3} [] [] {A : Matrix m m K} :
(LinearIndependent K fun (i : m) => )
theorem Matrix.vecMul_surjective_of_invertible {m : Type u} [] {R : Type u_2} [] [] (A : Matrix m m R) [] :
Function.Surjective fun (v : mR) =>
theorem Matrix.mulVec_surjective_of_invertible {m : Type u} [] {R : Type u_2} [] [] (A : Matrix m m R) [] :
theorem Matrix.vecMul_injective_of_invertible {m : Type u} [] {K : Type u_3} [] [] (A : Matrix m m K) [] :
Function.Injective fun (v : mK) =>
theorem Matrix.mulVec_injective_of_invertible {m : Type u} [] {K : Type u_3} [] [] (A : Matrix m m K) [] :
theorem Matrix.linearIndependent_rows_of_invertible {m : Type u} [] {K : Type u_3} [] [] (A : Matrix m m K) [] :
LinearIndependent K fun (i : m) => A i
theorem Matrix.linearIndependent_cols_of_invertible {m : Type u} [] {K : Type u_3} [] [] (A : Matrix m m K) [] :
LinearIndependent K fun (i : m) =>
theorem Matrix.nonsing_inv_cancel_or_zero {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) :
A⁻¹ * A = 1 A * A⁻¹ = 1 A⁻¹ = 0
theorem Matrix.det_nonsing_inv_mul_det {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :
= 1
@[simp]
theorem Matrix.det_nonsing_inv {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) :
theorem Matrix.isUnit_nonsing_inv_det {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :
@[simp]
theorem Matrix.nonsing_inv_nonsing_inv {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :
theorem Matrix.isUnit_nonsing_inv_det_iff {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} :
noncomputable def Matrix.invertibleOfIsUnitDet {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :

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

Equations
• = { invOf := A⁻¹, invOf_mul_self := , mul_invOf_self := }
Instances For
noncomputable def Matrix.nonsingInvUnit {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :
(Matrix n n α)ˣ

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

Equations
Instances For
theorem Matrix.unitOfDetInvertible_eq_nonsingInvUnit {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) [] :
theorem Matrix.inv_eq_left_inv {n : Type u'} {α : Type v} [] [] [] {A : Matrix n n α} {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} [] [] [] {A : Matrix n n α} {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} [] [] [] {A : Matrix n n α} {B : Matrix n n α} {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} [] [] [] {A : Matrix n n α} {B : Matrix n n α} {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} [] [] [] {A : Matrix n n α} {B : Matrix n n α} {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} [] [] [] {A : Matrix n n α} {B : Matrix n n α} (h : A⁻¹ = B⁻¹) (h' : IsUnit ()) :
A = B
@[simp]
theorem Matrix.inv_zero {n : Type u'} {α : Type v} [] [] [] :
0⁻¹ = 0
noncomputable instance Matrix.instInvOneClassMatrix {n : Type u'} {α : Type v} [] [] [] :
Equations
• Matrix.instInvOneClassMatrix = let __src := Matrix.one; let __src_1 := Matrix.inv;
theorem Matrix.inv_smul {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (k : α) [] (h : IsUnit ()) :
theorem Matrix.inv_smul' {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (k : αˣ) (h : IsUnit ()) :
theorem Matrix.inv_adjugate {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (h : IsUnit ()) :
= ()⁻¹ A
def Matrix.diagonalInvertible {n : Type u'} [] [] {α : Type u_2} [] (v : nα) [] :

diagonal v is invertible if v is

Equations
Instances For
theorem Matrix.invOf_diagonal_eq {n : Type u'} [] [] {α : Type u_2} [] (v : nα) [] [] :
def Matrix.invertibleOfDiagonalInvertible {n : Type u'} {α : Type v} [] [] [] (v : nα) [] :

v is invertible if diagonal v is

Equations
• = { invOf := , invOf_mul_self := , mul_invOf_self := }
Instances For
@[simp]
theorem Matrix.diagonalInvertibleEquivInvertible_symm_apply {n : Type u'} {α : Type v} [] [] [] (v : nα) [] :
inst✝ =
@[simp]
theorem Matrix.diagonalInvertibleEquivInvertible_apply {n : Type u'} {α : Type v} [] [] [] (v : nα) [] :
def Matrix.diagonalInvertibleEquivInvertible {n : Type u'} {α : Type v} [] [] [] (v : nα) :

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.
Instances For
@[simp]
theorem Matrix.isUnit_diagonal {n : Type u'} {α : Type v} [] [] [] {v : nα} :

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

theorem Matrix.inv_diagonal {n : Type u'} {α : Type v} [] [] [] (v : nα) :
@[simp]
theorem Matrix.inv_inv_inv {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) :
theorem Matrix.mul_inv_rev {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (B : Matrix n n α) :
(A * B)⁻¹ = B⁻¹ * A⁻¹
theorem Matrix.list_prod_inv_reverse {n : Type u'} {α : Type v} [] [] [] (l : List (Matrix n n α)) :
()⁻¹ = List.prod (List.map Inv.inv ())

A version of List.prod_inv_reverse for Matrix.inv.

@[simp]
theorem Matrix.det_smul_inv_mulVec_eq_cramer {n : Type u'} {α : Type v} [] [] [] (A : Matrix n n α) (b : nα) (h : IsUnit ()) :
= () 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} [] [] [] (A : Matrix n n α) (b : nα) (h : IsUnit ()) :
= 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} [] [] [] [] [] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) [] :
Invertible (Matrix.submatrix A e₁ e₂)

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

Equations
Instances For
def Matrix.invertibleOfSubmatrixEquivInvertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] [] [] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) [Invertible (Matrix.submatrix A e₁ e₂)] :

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

Equations
Instances For
theorem Matrix.invOf_submatrix_equiv_eq {m : Type u} {n : Type u'} {α : Type v} [] [] [] [] [] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) [] [Invertible (Matrix.submatrix A e₁ e₂)] :
(Matrix.submatrix A e₁ e₂) = Matrix.submatrix A e₂ e₁
@[simp]
theorem Matrix.submatrixEquivInvertibleEquivInvertible_apply {m : Type u} {n : Type u'} {α : Type v} [] [] [] [] [] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) :
∀ (x : Invertible (Matrix.submatrix A e₁ e₂)),
@[simp]
theorem Matrix.submatrixEquivInvertibleEquivInvertible_symm_apply {m : Type u} {n : Type u'} {α : Type v} [] [] [] [] [] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) :
∀ (x : ), .symm x =
def Matrix.submatrixEquivInvertibleEquivInvertible {m : Type u} {n : Type u'} {α : Type v} [] [] [] [] [] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) :
Invertible (Matrix.submatrix A e₁ e₂)

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.
Instances For
@[simp]
theorem Matrix.isUnit_submatrix_equiv {m : Type u} {n : Type u'} {α : Type v} [] [] [] [] [] {A : Matrix m m α} (e₁ : n m) (e₂ : n m) :
IsUnit (Matrix.submatrix A e₁ e₂)

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

@[simp]
theorem Matrix.inv_submatrix_equiv {m : Type u} {n : Type u'} {α : Type v} [] [] [] [] [] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) :
(Matrix.submatrix A e₁ e₂)⁻¹ = Matrix.submatrix A⁻¹ e₂ e₁
theorem Matrix.inv_reindex {m : Type u} {n : Type u'} {α : Type v} [] [] [] [] [] (e₁ : n m) (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} [] [] [] {M : Matrix m m α} (h : ) (N : Matrix m m α) :
Matrix.det (M * N * M⁻¹) =

A variant of Matrix.det_units_conj.

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

A variant of Matrix.det_units_conj'.