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⁻¹ (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:

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⁻¹

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 #

source

@[protected]

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

⅟ A ⬝ A = 1

A copy of inv_of_mul_self using ⬝ not *.

source

@[protected]

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

A ⬝ ⅟ A = 1

A copy of mul_inv_of_self using ⬝ not *.

source

@[protected]

theorem matrix.inv_of_mul_self_assoc {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : matrix n n α) (B : matrix n m α) [invertible A] :

⅟ A ⬝ (A ⬝ B) = B

A copy of inv_of_mul_self_assoc using ⬝ not *.

source

@[protected]

theorem matrix.mul_inv_of_self_assoc {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : matrix n n α) (B : matrix n m α) [invertible A] :

A ⬝ (⅟ A ⬝ B) = B

A copy of mul_inv_of_self_assoc using ⬝ not *.

source

@[protected]

theorem matrix.mul_inv_of_mul_self_cancel {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : matrix m n α) (B : matrix n n α) [invertible B] :

A ⬝ ⅟ B ⬝ B = A

A copy of mul_inv_of_mul_self_cancel using ⬝ not *.

source

@[protected]

theorem matrix.mul_mul_inv_of_self_cancel {m : Type u} {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : matrix m n α) (B : matrix n n α) [invertible B] :

A ⬝ B ⬝ ⅟ B = A

A copy of mul_mul_inv_of_self_cancel using ⬝ not *.

source

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

invertible A

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

Equations

A.invertible_of_det_invertible = {inv_of := ⅟ A.det • A.adjugate, inv_of_mul_self := _, mul_inv_of_self := _}

source

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

⅟ A = ⅟ A.det • A.adjugate

source

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

invertible A.det

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

Equations

A.det_invertible_of_left_inverse B h = {inv_of := B.det, inv_of_mul_self := _, mul_inv_of_self := _}

source

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

invertible A.det

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

Equations

A.det_invertible_of_right_inverse B h = {inv_of := B.det, inv_of_mul_self := _, mul_inv_of_self := _}

source

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

invertible A.det

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

Equations

A.det_invertible_of_invertible = A.det_invertible_of_left_inverse (⅟ A) _

source

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

(⅟ A).det = ⅟ A.det

source

@[simp]

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

⇑(A.invertible_equiv_det_invertible) _inst_4 = A.det_invertible_of_invertible

source

@[simp]

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

⇑(A.invertible_equiv_det_invertible.symm) _inst_4 = A.invertible_of_det_invertible

source

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

invertible A ≃ invertible A.det

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

A.invertible_equiv_det_invertible = {to_fun := A.det_invertible_of_invertible, inv_fun := A.invertible_of_det_invertible, left_inv := _, right_inv := _}

source

theorem matrix.mul_eq_one_comm {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : matrix n n α} :

A ⬝ B = 1 ↔ B ⬝ A = 1

source

def matrix.invertible_of_left_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (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.invertible_of_left_inverse B h = {inv_of := B, inv_of_mul_self := h, mul_inv_of_self := _}

source

def matrix.invertible_of_right_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (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.invertible_of_right_inverse B h = {inv_of := B, inv_of_mul_self := _, mul_inv_of_self := h}

source

def matrix.unit_of_det_invertible {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (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.unit_of_det_invertible = unit_of_invertible A

source

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

is_unit A ↔ is_unit A.det

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

Variants of the statements above with `is_unit` #

source

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

is_unit A.det

source

theorem matrix.is_unit_det_of_left_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : matrix n n α} (h : B ⬝ A = 1) :

is_unit A.det

source

theorem matrix.is_unit_det_of_right_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : matrix n n α} (h : A ⬝ B = 1) :

is_unit A.det

source

theorem matrix.det_ne_zero_of_left_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : matrix n n α} [nontrivial α] (h : B ⬝ A = 1) :

A.det ≠ 0

source

theorem matrix.det_ne_zero_of_right_inverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : matrix n n α} [nontrivial α] (h : A ⬝ B = 1) :

A.det ≠ 0

source

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

is_unit Aᵀ.det

A noncomputable `has_inv` instance #

source

@[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

matrix.has_inv = {inv := λ (A : matrix n n α), ring.inverse A.det • A.adjugate}

source

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

A⁻¹ = ring.inverse A.det • A.adjugate

source

theorem matrix.nonsing_inv_apply_not_is_unit {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : matrix n n α) (h : ¬is_unit A.det) :

A⁻¹ = 0

source

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

A⁻¹ = ↑(h.unit)⁻¹ • A.adjugate

source

@[simp]

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

⅟ A = A⁻¹

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

source

@[simp, norm_cast]

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

↑A⁻¹ = (↑A)⁻¹

Coercing the result of units.has_inv is the same as coercing first and applying the nonsingular inverse.

source

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

A⁻¹ = ring.inverse A

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

source

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

A⁻¹ ᵀ = Aᵀ ⁻¹

source

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

A⁻¹ ᴴ = Aᴴ ⁻¹

source

@[simp]

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

A ⬝ A⁻¹ = 1

The nonsing_inv of A is a right inverse.

source

@[simp]

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

A⁻¹ ⬝ A = 1

The nonsing_inv of A is a left inverse.

source

@[simp]

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

A ⬝ A⁻¹ = 1

source

@[simp]

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

A⁻¹ ⬝ A = 1

source

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

A⁻¹ ⬝ A = 1 ∧ A ⬝ A⁻¹ = 1 ∨ A⁻¹ = 0

source

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

(A⁻¹.det) * A.det = 1

source

@[simp]

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

A⁻¹.det = ring.inverse A.det

source

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

is_unit A⁻¹.det

source

@[simp]

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

A⁻¹ ⁻¹ = A

source

theorem matrix.is_unit_nonsing_inv_det_iff {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A : matrix n n α} :

is_unit A⁻¹.det ↔ is_unit A.det

source

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

invertible A

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

Equations

A.invertible_of_is_unit_det h = {inv_of := A⁻¹, inv_of_mul_self := _, mul_inv_of_self := _}

source

noncomputable def matrix.nonsing_inv_unit {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : matrix n 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

A.nonsing_inv_unit h = unit_of_invertible A

source

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

A.unit_of_det_invertible = A.nonsing_inv_unit _

source

theorem matrix.inv_eq_left_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : matrix n n α} (h : B ⬝ A = 1) :

A⁻¹ = B

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

source

theorem matrix.inv_eq_right_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : matrix n n α} (h : A ⬝ B = 1) :

A⁻¹ = B

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

source

theorem matrix.left_inv_eq_left_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {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.

source

theorem matrix.right_inv_eq_right_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {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.

source

theorem matrix.right_inv_eq_left_inv {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {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.

source

theorem matrix.inv_inj {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] {A B : matrix n n α} (h : A⁻¹ = B⁻¹) (h' : is_unit A.det) :

A = B

source

@[simp]

theorem matrix.inv_zero {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] :

0⁻¹ = 0

source

@[simp]

theorem matrix.inv_one {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] :

1⁻¹ = 1

source

theorem matrix.inv_smul {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : matrix n n α) (k : α) [invertible k] (h : is_unit A.det) :

(k • A)⁻¹ = ⅟ k • A⁻¹

source

theorem matrix.inv_smul' {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (A : matrix n n α) (k : αˣ) (h : is_unit A.det) :

(k • A)⁻¹ = k⁻¹ • A⁻¹

source

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

(A.adjugate)⁻¹ = (h.unit)⁻¹ • A

source

@[simp]

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

A⁻¹ ⁻¹ ⁻¹ = A⁻¹

source

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

(A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹

source

theorem matrix.list_prod_inv_reverse {n : Type u'} {α : Type v} [fintype n] [decidable_eq n] [comm_ring α] (l : list (matrix n n α)) :

(l.prod)⁻¹ = (list.map has_inv.inv l.reverse).prod

A version of list.prod_inv_reverse for matrix.has_inv.

source

@[simp]

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

A.det • A⁻¹.mul_vec b = ⇑(A.cramer) b

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

source

@[simp]

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

A.det • matrix.vec_mul b A⁻¹ = ⇑(Aᵀ.cramer) b

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

More results about determinants #

source

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

(M ⬝ N ⬝ M⁻¹).det = N.det

A variant of matrix.det_units_conj.

source

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

(M⁻¹ ⬝ N ⬝ M).det = N.det

A variant of matrix.det_units_conj'.

source

theorem matrix.det_from_blocks₁₁ {m : Type u} {n : Type u'} {α : Type v} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) [invertible A] :

(matrix.from_blocks A B C D).det = (A.det) * (D - C ⬝ ⅟ A ⬝ B).det

Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of the Schur complement.

source

@[simp]

theorem matrix.det_from_blocks_one₁₁ {m : Type u} {n : Type u'} {α : Type v} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) :

(matrix.from_blocks 1 B C D).det = (D - C ⬝ B).det

source

theorem matrix.det_from_blocks₂₂ {m : Type u} {n : Type u'} {α : Type v} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) (D : matrix n n α) [invertible D] :

(matrix.from_blocks A B C D).det = (D.det) * (A - B ⬝ ⅟ D ⬝ C).det

Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms of the Schur complement.

source

@[simp]

theorem matrix.det_from_blocks_one₂₂ {m : Type u} {n : Type u'} {α : Type v} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] [comm_ring α] (A : matrix m m α) (B : matrix m n α) (C : matrix n m α) :

(matrix.from_blocks A B C 1).det = (A - B ⬝ C).det

source

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

(1 + A ⬝ B).det = (1 + B ⬝ A).det

The Weinstein–Aronszajn identity. Note the 1 on the LHS is of shape m×m, while the 1 on the RHS is of shape n×n.

source

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

(A ⬝ B + 1).det = (B ⬝ A + 1).det

Alternate statement of the Weinstein–Aronszajn identity

source

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

(1 - A ⬝ B).det = (1 - B ⬝ A).det

source

theorem matrix.det_one_add_col_mul_row {m : Type u} {α : Type v} [fintype m] [decidable_eq m] [comm_ring α] (u v : m → α) :

(1 + matrix.col u ⬝ matrix.row v).det = 1 + v ⬝ᵥ u

A special case of the Matrix determinant lemma for when A = I.

TODO: show this more generally.

Nonsingular inverses #

References #

Tags #

Matrices are invertible iff their determinants are #

Variants of the statements above with is_unit #

A noncomputable has_inv instance #

More results about determinants #

Matrices are `invertible` iff their determinants are #

Variants of the statements above with `is_unit` #

A noncomputable `has_inv` instance #