Documentation

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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:

We start by working with Invertible, and show the main results:

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 #

Tags #

matrix inverse, cramer, cramer's rule, adjugate

Matrices are Invertible iff their determinants are #

def Matrix.invertibleOfDetInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A.det] :

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

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

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

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

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

      Equations
      • A.detInvertibleOfRightInverse B h = { invOf := B.det, invOf_mul_self := , mul_invOf_self := }
      Instances For
        def Matrix.detInvertibleOfInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :

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

        Equations
        • A.detInvertibleOfInvertible = A.detInvertibleOfLeftInverse A
        Instances For
          theorem Matrix.det_invOf {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] [Invertible A.det] :
          (A).det = A.det
          @[simp]
          theorem Matrix.invertibleEquivDetInvertible_symm_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A.det] :
          A.invertibleEquivDetInvertible.symm inst✝ = A.invertibleOfDetInvertible
          @[simp]
          theorem Matrix.invertibleEquivDetInvertible_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :
          A.invertibleEquivDetInvertible inst✝ = A.detInvertibleOfInvertible
          def Matrix.invertibleEquivDetInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (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} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} :
            A * B = 1 B * A = 1
            def Matrix.invertibleOfLeftInverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (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
            • A.invertibleOfLeftInverse B h = { invOf := B, invOf_mul_self := h, mul_invOf_self := }
            Instances For
              def Matrix.invertibleOfRightInverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (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
              • A.invertibleOfRightInverse B h = { invOf := B, invOf_mul_self := , mul_invOf_self := h }
              Instances For
                def Matrix.unitOfDetInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (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
                Instances For
                  theorem Matrix.isUnit_iff_isUnit_det {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) :
                  IsUnit A IsUnit A.det

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

                  @[simp]
                  theorem Matrix.isUnits_det_units {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : (Matrix n n α)ˣ) :
                  IsUnit (↑A).det

                  Variants of the statements above with IsUnit #

                  theorem Matrix.isUnit_det_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :
                  IsUnit A.det
                  theorem Matrix.isUnit_of_left_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} (h : B * A = 1) :
                  theorem Matrix.exists_left_inverse_iff_isUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} :
                  (∃ (B : Matrix n n α), B * A = 1) IsUnit A
                  theorem Matrix.isUnit_of_right_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} (h : A * B = 1) :
                  theorem Matrix.exists_right_inverse_iff_isUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} :
                  (∃ (B : Matrix n n α), A * B = 1) IsUnit A
                  theorem Matrix.isUnit_det_of_left_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} (h : B * A = 1) :
                  IsUnit A.det
                  theorem Matrix.isUnit_det_of_right_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} (h : A * B = 1) :
                  IsUnit A.det
                  theorem Matrix.det_ne_zero_of_left_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} [Nontrivial α] (h : B * A = 1) :
                  A.det 0
                  theorem Matrix.det_ne_zero_of_right_inverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} [Nontrivial α] (h : A * B = 1) :
                  A.det 0
                  theorem Matrix.mul_eq_one_comm_of_equiv {m : Type u} {n : Type u'} {α : Type v} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m n α} {B : Matrix n m α} (e : m n) :
                  A * B = 1 B * A = 1

                  A version of mul_eq_one_comm that works for square matrices with rectangular types.

                  theorem Matrix.isUnit_det_transpose {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :
                  IsUnit A.transpose.det

                  A noncomputable Inv instance #

                  noncomputable instance Matrix.inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] :
                  Inv (Matrix n n α)

                  The inverse of a square matrix, when it is invertible (and zero otherwise).

                  Equations
                  theorem Matrix.inv_def {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) :
                  A⁻¹ = Ring.inverse A.det A.adjugate
                  theorem Matrix.nonsing_inv_apply_not_isUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : ¬IsUnit A.det) :
                  A⁻¹ = 0
                  theorem Matrix.nonsing_inv_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :
                  A⁻¹ = h.unit⁻¹ A.adjugate
                  @[simp]
                  theorem Matrix.invOf_eq_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :

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

                  @[simp]
                  theorem Matrix.coe_units_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (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} [Fintype n] [DecidableEq n] [CommRing α] (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} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) :
                  A⁻¹.transpose = A.transpose⁻¹
                  theorem Matrix.conjTranspose_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [StarRing α] :
                  A⁻¹.conjTranspose = A.conjTranspose⁻¹
                  @[simp]
                  theorem Matrix.mul_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :
                  A * A⁻¹ = 1

                  The nonsing_inv of A is a right inverse.

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

                  The nonsing_inv of A is a left inverse.

                  instance Matrix.instInvertibleInv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :
                  Equations
                  • A.instInvertibleInv = .mpr inferInstance
                  @[simp]
                  theorem Matrix.inv_inv_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :
                  @[simp]
                  theorem Matrix.mul_nonsing_inv_cancel_right {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix m n α) (h : IsUnit A.det) :
                  B * A * A⁻¹ = B
                  @[simp]
                  theorem Matrix.mul_nonsing_inv_cancel_left {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n m α) (h : IsUnit A.det) :
                  A * (A⁻¹ * B) = B
                  @[simp]
                  theorem Matrix.nonsing_inv_mul_cancel_right {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix m n α) (h : IsUnit A.det) :
                  B * A⁻¹ * A = B
                  @[simp]
                  theorem Matrix.nonsing_inv_mul_cancel_left {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n m α) (h : IsUnit A.det) :
                  A⁻¹ * (A * B) = B
                  @[simp]
                  theorem Matrix.mul_inv_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :
                  A * A⁻¹ = 1
                  @[simp]
                  theorem Matrix.inv_mul_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :
                  A⁻¹ * A = 1
                  @[simp]
                  theorem Matrix.mul_inv_cancel_right_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix m n α) [Invertible A] :
                  B * A * A⁻¹ = B
                  @[simp]
                  theorem Matrix.mul_inv_cancel_left_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
                  A * (A⁻¹ * B) = B
                  @[simp]
                  theorem Matrix.inv_mul_cancel_right_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix m n α) [Invertible A] :
                  B * A⁻¹ * A = B
                  @[simp]
                  theorem Matrix.inv_mul_cancel_left_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
                  A⁻¹ * (A * B) = B
                  theorem Matrix.inv_mul_eq_iff_eq_mul_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n n α) (C : Matrix n n α) [Invertible A] :
                  A⁻¹ * B = C B = A * C
                  theorem Matrix.mul_inv_eq_iff_eq_mul_of_invertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n n α) (C : Matrix n n α) [Invertible A] :
                  B * A⁻¹ = C B = C * A
                  theorem Matrix.inv_mulVec_eq_vec {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} [Invertible A] {u : nα} {v : nα} (hM : u = A.mulVec v) :
                  A⁻¹.mulVec u = v
                  theorem Matrix.mul_right_injective_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :
                  Function.Injective fun (x : Matrix n m α) => A * x
                  theorem Matrix.mul_left_injective_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] :
                  Function.Injective fun (x : Matrix m n α) => x * A
                  theorem Matrix.mul_right_inj_of_invertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] {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} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] {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} [Fintype n] [Fintype m] [DecidableEq m] [CommRing α] (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} [Fintype n] [Fintype m] [DecidableEq m] [CommRing α] (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} [Semiring R] [DecidableEq n] [Fintype m] [Finite n] {A : Matrix m n R} :
                  (Function.Surjective fun (v : mR) => Matrix.vecMul v A) ∃ (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} [Semiring R] [DecidableEq m] [Finite m] [Fintype n] {A : Matrix m n R} :
                  Function.Surjective A.mulVec ∃ (B : Matrix n m R), A * B = 1
                  theorem Matrix.vecMul_surjective_iff_isUnit {m : Type u} [DecidableEq m] {R : Type u_2} [CommRing R] [Fintype m] {A : Matrix m m R} :
                  (Function.Surjective fun (v : mR) => Matrix.vecMul v A) IsUnit A
                  theorem Matrix.vecMul_injective_iff_isUnit {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] {A : Matrix m m K} :
                  (Function.Injective fun (v : mK) => Matrix.vecMul v A) IsUnit A
                  theorem Matrix.mulVec_injective_iff_isUnit {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] {A : Matrix m m K} :
                  theorem Matrix.linearIndependent_rows_iff_isUnit {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] {A : Matrix m m K} :
                  (LinearIndependent K fun (i : m) => A i) IsUnit A
                  theorem Matrix.linearIndependent_cols_iff_isUnit {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] {A : Matrix m m K} :
                  (LinearIndependent K fun (i : m) => A.transpose i) IsUnit A
                  theorem Matrix.vecMul_surjective_of_invertible {m : Type u} [DecidableEq m] {R : Type u_2} [CommRing R] [Fintype m] (A : Matrix m m R) [Invertible A] :
                  Function.Surjective fun (v : mR) => Matrix.vecMul v A
                  theorem Matrix.vecMul_injective_of_invertible {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] (A : Matrix m m K) [Invertible A] :
                  Function.Injective fun (v : mK) => Matrix.vecMul v A
                  theorem Matrix.mulVec_injective_of_invertible {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] (A : Matrix m m K) [Invertible A] :
                  theorem Matrix.linearIndependent_rows_of_invertible {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] (A : Matrix m m K) [Invertible A] :
                  LinearIndependent K fun (i : m) => A i
                  theorem Matrix.linearIndependent_cols_of_invertible {m : Type u} [DecidableEq m] {K : Type u_3} [Field K] [Fintype m] (A : Matrix m m K) [Invertible A] :
                  LinearIndependent K fun (i : m) => A.transpose i
                  theorem Matrix.nonsing_inv_cancel_or_zero {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) :
                  A⁻¹ * A = 1 A * A⁻¹ = 1 A⁻¹ = 0
                  theorem Matrix.det_nonsing_inv_mul_det {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :
                  A⁻¹.det * A.det = 1
                  @[simp]
                  theorem Matrix.det_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) :
                  A⁻¹.det = Ring.inverse A.det
                  theorem Matrix.isUnit_nonsing_inv_det {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :
                  @[simp]
                  theorem Matrix.nonsing_inv_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :
                  theorem Matrix.isUnit_nonsing_inv_det_iff {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} :
                  IsUnit A⁻¹.det IsUnit A.det
                  @[simp]
                  theorem Matrix.isUnit_nonsing_inv_iff {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} :
                  noncomputable def Matrix.invertibleOfIsUnitDet {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :

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

                  Equations
                  • A.invertibleOfIsUnitDet h = { invOf := A⁻¹, invOf_mul_self := , mul_invOf_self := }
                  Instances For
                    noncomputable def Matrix.nonsingInvUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :
                    (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} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A.det] :
                      A.unitOfDetInvertible = A.nonsingInvUnit
                      theorem Matrix.inv_eq_left_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {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} [Fintype n] [DecidableEq n] [CommRing α] {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} [Fintype n] [DecidableEq n] [CommRing α] {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} [Fintype n] [DecidableEq n] [CommRing α] {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} [Fintype n] [DecidableEq n] [CommRing α] {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} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) :
                      A = B
                      @[simp]
                      theorem Matrix.inv_zero {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] :
                      0⁻¹ = 0
                      noncomputable instance Matrix.instInvOneClass {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] :
                      Equations
                      theorem Matrix.inv_smul {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (k : α) [Invertible k] (h : IsUnit A.det) :
                      theorem Matrix.inv_smul' {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (k : αˣ) (h : IsUnit A.det) :
                      theorem Matrix.inv_adjugate {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit A.det) :
                      A.adjugate⁻¹ = h.unit⁻¹ A
                      def Matrix.diagonalInvertible {n : Type u'} [Fintype n] [DecidableEq n] {α : Type u_2} [NonAssocSemiring α] (v : nα) [Invertible v] :

                      diagonal v is invertible if v is

                      Equations
                      Instances For

                        v is invertible if diagonal v is

                        Equations
                        Instances For

                          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} [Fintype n] [DecidableEq n] [CommRing α] {v : nα} :

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

                            theorem Matrix.inv_diagonal {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (v : nα) :
                            @[simp]
                            theorem Matrix.inv_subsingleton {m : Type u} {α : Type v} [CommRing α] [Subsingleton m] [Fintype m] [DecidableEq m] (A : Matrix m m α) :
                            A⁻¹ = Matrix.diagonal fun (i : m) => Ring.inverse (A i i)

                            The inverse of a 1×1 or 0×0 matrix is always diagonal.

                            While we could write this as of fun _ _ => Ring.inverse (A default default) on the RHS, this is less useful because:

                            • It wouldn't work for 0×0 matrices.
                            • More things are true about diagonal matrices than constant matrices, and so more lemmas exist.

                            Matrix.diagonal_unique can be used to reach this form, while Ring.inverse_eq_inv can be used to replace Ring.inverse with ⁻¹.

                            theorem Matrix.add_mul_mul_inv_eq_sub {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) :
                            (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

                            The Woodbury Identity (⁻¹ version).

                            @[simp]
                            theorem Matrix.inv_inv_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) :
                            theorem Matrix.inv_add_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} (h : IsUnit A IsUnit B) :
                            A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹

                            The Matrix version of inv_add_inv'

                            theorem Matrix.inv_sub_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] {A : Matrix n n α} {B : Matrix n n α} (h : IsUnit A IsUnit B) :
                            A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹

                            The Matrix version of inv_sub_inv'

                            theorem Matrix.mul_inv_rev {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (B : Matrix n n α) :
                            (A * B)⁻¹ = B⁻¹ * A⁻¹
                            theorem Matrix.list_prod_inv_reverse {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (l : List (Matrix n n α)) :
                            l.prod⁻¹ = (List.map Inv.inv l.reverse).prod

                            A version of List.prod_inv_reverse for Matrix.inv.

                            @[simp]
                            theorem Matrix.det_smul_inv_mulVec_eq_cramer {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (b : nα) (h : IsUnit A.det) :
                            A.det A⁻¹.mulVec b = A.cramer 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} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (b : nα) (h : IsUnit A.det) :
                            A.det Matrix.vecMul b A⁻¹ = A.transpose.cramer 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} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) [Invertible A] :
                            Invertible (A.submatrix e₁ e₂)

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

                            Equations
                            • A.submatrixEquivInvertible e₁ e₂ = (A.submatrix e₁ e₂).invertibleOfRightInverse ((A).submatrix e₂ e₁)
                            Instances For
                              def Matrix.invertibleOfSubmatrixEquivInvertible {m : Type u} {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) (e₁ : n m) (e₂ : n m) [Invertible (A.submatrix e₁ e₂)] :

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

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

                                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} [Fintype n] [DecidableEq n] [CommRing α] [Fintype m] [DecidableEq m] {A : Matrix m m α} (e₁ : n m) (e₂ : n m) :
                                  IsUnit (A.submatrix e₁ e₂) IsUnit A

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

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

                                  A variant of Matrix.det_units_conj.

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

                                  A variant of Matrix.det_units_conj'.

                                  More results about traces #

                                  theorem Matrix.trace_conj {m : Type u} {α : Type v} [CommRing α] [Fintype m] [DecidableEq m] {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
                                  (M * N * M⁻¹).trace = N.trace

                                  A variant of Matrix.trace_units_conj.

                                  theorem Matrix.trace_conj' {m : Type u} {α : Type v} [CommRing α] [Fintype m] [DecidableEq m] {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
                                  (M⁻¹ * N * M).trace = N.trace

                                  A variant of Matrix.trace_units_conj'.