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_cancel_left {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_cancel_left for rectangular matrices.

source
theorem Matrix.mul_invOf_cancel_left {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_cancel_left for rectangular matrices.

source
theorem Matrix.invOf_mul_cancel_right {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 invOf_mul_cancel_right for rectangular matrices.

source
theorem Matrix.mul_invOf_cancel_right {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_cancel_right for rectangular matrices.

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

A copy oy of invOf_mul_eq_iff_eq_mul_left for rectangular matrices.

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

A copy oy of mul_left_eq_iff_eq_invOf_mul for rectangular matrices.

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

A copy oy of mul_invOf_eq_iff_eq_mul_right for rectangular matrices.

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

A copy oy of mul_right_eq_iff_eq_mul_invOf 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 A.conjTranspose

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 A.conjTranspose] :
(⅟A).conjTranspose = ⅟A.conjTranspose
source
def Matrix.invertibleOfInvertibleConjTranspose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Semiring α] [StarRing α] (A : Matrix n n α) [Invertible A.conjTranspose] :
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 A.conjTranspose ↔ 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 A.transpose

    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 A.transpose] :
    (⅟A).transpose = ⅟A.transpose
    source
    def Matrix.invertibleOfInvertibleTranspose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) [Invertible A.transpose] :
    Invertible A

    Aᵀ is invertible when A is.

    Equations
    Instances For
      source
      def Matrix.transposeInvertibleEquivInvertible {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) :
      Invertible A.transpose ≃ 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.transposeInvertibleEquivInvertible_symm_apply {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) [Invertible A] :
        A.transposeInvertibleEquivInvertible.symm inst✝ = A.invertibleTranspose
        source
        @[simp]
        theorem Matrix.transposeInvertibleEquivInvertible_apply {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) [Invertible A.transpose] :
        A.transposeInvertibleEquivInvertible inst✝ = A.invertibleOfInvertibleTranspose
        source
        @[simp]
        theorem Matrix.isUnit_transpose {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring α] (A : Matrix n n α) :
        IsUnit A.transpose ↔ IsUnit A
        source
        theorem Matrix.add_mul_mul_invOf_mul_eq_one {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)] :
        (A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) = 1
        source
        theorem Matrix.add_mul_mul_invOf_mul_eq_one' {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)] :
        (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) * (A + U * C * V) = 1

        Like add_mul_mul_invOf_mul_eq_one, but with multiplication reversed.

        source
        def Matrix.invertibleAddMulMul {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)] :
        Invertible (A + U * C * V)

        If matrices A, C, and C⁻¹ + V * A⁻¹ * U are invertible, then so is A + U * C * V.

        Equations
        Instances For
          source
          theorem Matrix.invOf_add_mul_mul {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)] [Invertible (A + U * C * V)] :
          ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

          The Woodbury Identity (⅟ version).

          See Matrix.invOf_add_mul_mul' for the Binomial Inverse Theorem.

          source
          theorem Matrix.add_mul_mul_mul_invOf_eq_one {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible (C + C * V * ⅟A * U * C)] :
          (A + U * C * V) * (⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) = 1
          source
          theorem Matrix.add_mul_mul_mul_invOf_eq_one' {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible (C + C * V * ⅟A * U * C)] :
          (⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) * (A + U * C * V) = 1
          source
          def Matrix.invertibleAddMulMul' {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible (C + C * V * ⅟A * U * C)] :
          Invertible (A + U * C * V)

          If matrices A and C + C * V * A⁻¹ * U * C are invertible, then so is A + U * C * V.

          Equations
          Instances For
            source
            theorem Matrix.invOf_add_mul_mul' {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) [Invertible A] [Invertible (C + C * V * ⅟A * U * C)] [Invertible (A + U * C * V)] :
            ⅟(A + U * C * V) = ⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A

            The Binomial Inverse Theorem (⅟ version).

            See Matrix.invOf_add_mul_mul for the Woodbury identity.