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 #

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Matrix.invOf_eq {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible (Matrix.det A)] [Invertible A] :
    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
    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
      Instances For

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

        Equations
        Instances For
          theorem Matrix.det_invOf {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible A] [Invertible (Matrix.det A)] :

          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
            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
              Instances For
                def Matrix.unitOfDetInvertible {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) [Invertible (Matrix.det A)] :
                (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 α) :

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

                  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] :
                  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) :
                  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) :
                  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) :
                  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 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 α) :
                  theorem Matrix.nonsing_inv_apply_not_isUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : ¬IsUnit (Matrix.det A)) :
                  A⁻¹ = 0
                  theorem Matrix.nonsing_inv_apply {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit (Matrix.det A)) :
                  @[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.

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

                  The nonsing_inv of A is a left inverse.

                  @[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 (Matrix.det A)) :
                  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 (Matrix.det A)) :
                  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 (Matrix.det A)) :
                  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 (Matrix.det A)) :
                  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.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] [CommRing α] [Fintype m] [DecidableEq m] (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] [CommRing α] [Fintype m] [DecidableEq m] (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'} [Fintype n] [DecidableEq n] [Fintype m] {R : Type u_3} [Semiring R] {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'} [Fintype n] [Fintype m] [DecidableEq m] {R : Type u_3} [Semiring R] {A : Matrix m n R} :
                  Function.Surjective (Matrix.mulVec A) ∃ (B : Matrix n m R), A * B = 1
                  theorem Matrix.vecMul_surjective_iff_isUnit {m : Type u} {α : Type v} [CommRing α] [Fintype m] [DecidableEq m] {A : Matrix m m α} :
                  (Function.Surjective fun (v : mα) => Matrix.vecMul v A) IsUnit A
                  theorem Matrix.vecMul_injective_iff_isUnit {m : Type u} [Fintype m] [DecidableEq m] {K : Type u_2} [Field K] {A : Matrix m m K} :
                  (Function.Injective fun (v : mK) => Matrix.vecMul v A) IsUnit A
                  theorem Matrix.linearIndependent_rows_iff_isUnit {m : Type u} [Fintype m] [DecidableEq m] {K : Type u_2} [Field K] {A : Matrix m m K} :
                  (LinearIndependent K fun (i : m) => A i) IsUnit A
                  theorem Matrix.linearIndependent_cols_iff_isUnit {m : Type u} [Fintype m] [DecidableEq m] {K : Type u_2} [Field K] {A : Matrix m m K} :
                  (LinearIndependent K fun (i : m) => Matrix.transpose A i) IsUnit A
                  theorem Matrix.vecMul_surjective_of_invertible {m : Type u} {α : Type v} [CommRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) [Invertible A] :
                  Function.Surjective fun (v : mα) => Matrix.vecMul v A
                  theorem Matrix.vecMul_injective_of_invertible {m : Type u} [Fintype m] [DecidableEq m] {K : Type u_2} [Field K] (A : Matrix m m K) [Invertible A] :
                  Function.Injective fun (v : mK) => Matrix.vecMul v A
                  theorem Matrix.linearIndependent_rows_of_invertible {m : Type u} [Fintype m] [DecidableEq m] {K : Type u_2} [Field K] (A : Matrix m m K) [Invertible A] :
                  LinearIndependent K fun (i : m) => A 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 (Matrix.det A)) :
                  @[simp]
                  theorem Matrix.det_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) :
                  theorem Matrix.isUnit_nonsing_inv_det {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit (Matrix.det A)) :
                  @[simp]
                  theorem Matrix.nonsing_inv_nonsing_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit (Matrix.det A)) :
                  noncomputable def Matrix.invertibleOfIsUnitDet {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit (Matrix.det A)) :

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

                  Equations
                  Instances For
                    noncomputable def Matrix.nonsingInvUnit {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit (Matrix.det A)) :
                    (Matrix n n α)ˣ

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

                    Equations
                    Instances For
                      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 (Matrix.det A)) :
                      A = B
                      @[simp]
                      theorem Matrix.inv_zero {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] :
                      0⁻¹ = 0
                      noncomputable instance Matrix.instInvOneClassMatrix {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] :
                      Equations
                      • Matrix.instInvOneClassMatrix = let src := Matrix.one; let src_1 := Matrix.inv; InvOneClass.mk (_ : 1⁻¹ = 1)
                      theorem Matrix.inv_smul {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (k : α) [Invertible k] (h : IsUnit (Matrix.det A)) :
                      theorem Matrix.inv_smul' {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (k : αˣ) (h : IsUnit (Matrix.det A)) :
                      theorem Matrix.inv_adjugate {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) (h : IsUnit (Matrix.det 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
                        • One or more equations did not get rendered due to their size.
                        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_inv_inv {n : Type u'} {α : Type v} [Fintype n] [DecidableEq n] [CommRing α] (A : Matrix n n α) :
                            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 α)) :

                            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 (Matrix.det A)) :

                            One form of Cramer's rule. See Matrix.mulVec_cramer for a stronger form.

                            @[simp]

                            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 (Matrix.submatrix A e₁ e₂)

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            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 (Matrix.submatrix A e₁ e₂)] :

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

                              Equations
                              • One or more equations did not get rendered due to their size.
                              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 (Matrix.submatrix A e₁ e₂)] :
                                (Matrix.submatrix A e₁ e₂) = Matrix.submatrix A 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) :
                                @[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) :
                                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) :

                                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 (Matrix.submatrix A 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) :
                                  (Matrix.submatrix A e₁ e₂)⁻¹ = Matrix.submatrix A⁻¹ 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 α) :

                                  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 α) :

                                  A variant of Matrix.det_units_conj'.