# Extra lemmas about invertible matrices #

A few of the Invertible lemmas generalize to multiplication of rectangular matrices.

For lemmas about the matrix inverse in terms of the determinant and adjugate, see Matrix.inv in LinearAlgebra/Matrix/NonsingularInverse.lean.

## Main results #

• Matrix.invertibleConjTranspose
• Matrix.invertibleTranspose
• Matrix.isUnit_conjTranpose
• Matrix.isUnit_tranpose
theorem Matrix.invOf_mul_self_assoc {m : Type u_1} {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) (B : Matrix n m α) [] :
A * (A * B) = B

A copy of invOf_mul_self_assoc for rectangular matrices.

theorem Matrix.mul_invOf_self_assoc {m : Type u_1} {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) (B : Matrix n m α) [] :
A * (A * B) = B

A copy of mul_invOf_self_assoc for rectangular matrices.

theorem Matrix.mul_invOf_mul_self_cancel {m : Type u_1} {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix m n α) (B : Matrix n n α) [] :
A * B * B = A

A copy of mul_invOf_mul_self_cancel for rectangular matrices.

theorem Matrix.mul_mul_invOf_self_cancel {m : Type u_1} {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix m n α) (B : Matrix n n α) [] :
A * B * B = A

A copy of mul_mul_invOf_self_cancel for rectangular matrices.

instance Matrix.invertibleConjTranspose {n : Type u_2} {α : Type u_3} [] [] [] [] (A : Matrix n n α) [] :
Invertible A.conjTranspose

The conjugate transpose of an invertible matrix is invertible.

Equations
• A.invertibleConjTranspose =
theorem Matrix.conjTranspose_invOf {n : Type u_2} {α : Type u_3} [] [] [] [] (A : Matrix n n α) [] [Invertible A.conjTranspose] :
(A).conjTranspose = A.conjTranspose
def Matrix.invertibleOfInvertibleConjTranspose {n : Type u_2} {α : Type u_3} [] [] [] [] (A : Matrix n n α) [Invertible A.conjTranspose] :

A matrix is invertible if the conjugate transpose is invertible.

Equations
• A.invertibleOfInvertibleConjTranspose = .mpr (.mpr inferInstance)
Instances For
@[simp]
theorem Matrix.isUnit_conjTranspose {n : Type u_2} {α : Type u_3} [] [] [] [] (A : Matrix n n α) :
IsUnit A.conjTranspose
instance Matrix.invertibleTranspose {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) [] :
Invertible A.transpose

The transpose of an invertible matrix is invertible.

Equations
• A.invertibleTranspose = { invOf := (A).transpose, invOf_mul_self := , mul_invOf_self := }
theorem Matrix.transpose_invOf {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) [] [Invertible A.transpose] :
(A).transpose = A.transpose
def Matrix.invertibleOfInvertibleTranspose {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) [Invertible A.transpose] :

Aᵀ is invertible when A is.

Equations
• A.invertibleOfInvertibleTranspose = { invOf := (A.transpose).transpose, invOf_mul_self := , mul_invOf_self := }
Instances For
@[simp]
theorem Matrix.transposeInvertibleEquivInvertible_apply {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) [Invertible A.transpose] :
A.transposeInvertibleEquivInvertible inst✝ = A.invertibleOfInvertibleTranspose
@[simp]
theorem Matrix.transposeInvertibleEquivInvertible_symm_apply {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) [] :
A.transposeInvertibleEquivInvertible.symm inst✝ = A.invertibleTranspose
def Matrix.transposeInvertibleEquivInvertible {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) :
Invertible A.transpose

Together Matrix.invertibleTranspose and Matrix.invertibleOfInvertibleTranspose 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_transpose {n : Type u_2} {α : Type u_3} [] [] [] (A : Matrix n n α) :
IsUnit A.transpose