Documentation

Mathlib.Data.Matrix.Invertible

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 #

source
theorem Matrix.invOf_mul_self_assoc {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
⅟A * (A * B) = B

A copy of invOf_mul_self_assoc for rectangular matrices.

source
theorem Matrix.mul_invOf_self_assoc {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
A * (⅟A * B) = B

A copy of mul_invOf_self_assoc for rectangular matrices.

source
theorem Matrix.mul_invOf_mul_self_cancel {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
A * ⅟B * B = A

A copy of mul_invOf_mul_self_cancel for rectangular matrices.

source
theorem Matrix.mul_mul_invOf_self_cancel {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
A * B * ⅟B = A

A copy of mul_mul_invOf_self_cancel for rectangular matrices.

source
instance Matrix.invertibleConjTranspose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] [StarRing α] (A : Matrix n n α) [Invertible A] :
Invertible (Matrix.conjTranspose A)

The conjugate transpose of an invertible matrix is invertible.

Equations
source
theorem Matrix.conjTranspose_invOf {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] [StarRing α] (A : Matrix n n α) [Invertible A] [Invertible (Matrix.conjTranspose A)] :
Matrix.conjTranspose ⅟A = ⅟(Matrix.conjTranspose A)
source
def Matrix.invertibleOfInvertibleConjTranspose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] [StarRing α] (A : Matrix n n α) [Invertible (Matrix.conjTranspose A)] :
Invertible A

A matrix is invertible if the conjugate transpose is invertible.

Equations
Instances For
    source
    @[simp]
    theorem Matrix.isUnit_conjTranspose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] [StarRing α] (A : Matrix n n α) :
    IsUnit (Matrix.conjTranspose A) ↔ IsUnit A
    source
    instance Matrix.invertibleTranspose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) [Invertible A] :
    Invertible (Matrix.transpose A)

    The transpose of an invertible matrix is invertible.

    Equations
    source
    theorem Matrix.transpose_invOf {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) [Invertible A] [Invertible (Matrix.transpose A)] :
    Matrix.transpose ⅟A = ⅟(Matrix.transpose A)
    source
    def Matrix.invertibleOfInvertibleTranspose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) [Invertible (Matrix.transpose A)] :
    Invertible A

    Aᵀ is invertible when A is.

    Equations
    Instances For
      source
      @[simp]
      theorem Matrix.transposeInvertibleEquivInvertible_apply {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) [Invertible (Matrix.transpose A)] :
      (Matrix.transposeInvertibleEquivInvertible A) inst✝ = Matrix.invertibleOfInvertibleTranspose A
      source
      @[simp]
      theorem Matrix.transposeInvertibleEquivInvertible_symm_apply {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) [Invertible A] :
      (Matrix.transposeInvertibleEquivInvertible A).symm inst✝ = Matrix.invertibleTranspose A
      source
      def Matrix.transposeInvertibleEquivInvertible {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) :
      Invertible (Matrix.transpose A) ≃ Invertible A

      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
        source
        @[simp]
        theorem Matrix.isUnit_transpose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) :
        IsUnit (Matrix.transpose A) ↔ IsUnit A