Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Matrix.invertibleOfDetInvertible definition

[Invertible A.det] : Invertible A

Full source

/-- If `A.det` has a constructive inverse, produce one for `A`. -/
def invertibleOfDetInvertible [Invertible A.det] : Invertible A where
  invOf := ⅟ A.det • A.adjugate
  mul_invOf_self := by
    rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]
  invOf_mul_self := by
    rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]

Invertibility of matrix from invertible determinant

Informal description

Given a square matrix $ A $ over a commutative ring, if the determinant $ \det A $ has a multiplicative inverse, then $ A $ is invertible with inverse $ A^{-1} = (\det A)^{-1} \cdot \text{adj}(A) $, where $ \text{adj}(A) $ is the adjugate matrix of $ A $.

Matrix.invOf_eq theorem

[Invertible A.det] [Invertible A] : ⅟ A = ⅟ A.det • A.adjugate

Full source

theorem invOf_eq [Invertible A.det] [Invertible A] : ⅟ A = ⅟ A.det • A.adjugate := by
  letI := invertibleOfDetInvertible A
  convert (rfl : ⅟ A = _)

Matrix Inverse Formula via Adjugate and Determinant

Informal description

Let $A$ be an $n \times n$ matrix over a commutative ring such that $\det A$ is invertible and $A$ itself is invertible. Then the inverse of $A$ is given by: \[ A^{-1} = (\det A)^{-1} \cdot \text{adj}(A) \] where $\text{adj}(A)$ denotes the adjugate matrix of $A$.

Matrix.detInvertibleOfLeftInverse definition

(h : B * A = 1) : Invertible A.det

Full source

/-- `A.det` is invertible if `A` has a left inverse. -/
def detInvertibleOfLeftInverse (h : B * A = 1) : Invertible A.det where
  invOf := B.det
  mul_invOf_self := by rw [mul_comm, ← det_mul, h, det_one]
  invOf_mul_self := by rw [← det_mul, h, det_one]

Invertibility of determinant from left inverse

Informal description

Given square matrices $A$ and $B$ over a ring $R$ such that $BA = I$, the determinant of $A$ is invertible in $R$.

Matrix.detInvertibleOfRightInverse definition

(h : A * B = 1) : Invertible A.det

Full source

/-- `A.det` is invertible if `A` has a right inverse. -/
def detInvertibleOfRightInverse (h : A * B = 1) : Invertible A.det where
  invOf := B.det
  mul_invOf_self := by rw [← det_mul, h, det_one]
  invOf_mul_self := by rw [mul_comm, ← det_mul, h, det_one]

Invertibility of determinant from right inverse

Informal description

Given square matrices $A$ and $B$ over a ring $R$ such that $AB = I$, the determinant of $A$ is invertible in $R$, with the inverse given by the determinant of $B$.

Matrix.detInvertibleOfInvertible definition

[Invertible A] : Invertible A.det

Full source

/-- If `A` has a constructive inverse, produce one for `A.det`. -/
def detInvertibleOfInvertible [Invertible A] : Invertible A.det :=
  detInvertibleOfLeftInverse A (⅟ A) (invOf_mul_self _)

Invertibility of determinant for invertible matrices

Informal description

Given a square matrix $A$ over a ring $R$ that has a multiplicative inverse (i.e., $A$ is invertible), the determinant of $A$ is also invertible in $R$.

Matrix.det_invOf theorem

[Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det

Full source

theorem det_invOf [Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det := by
  letI := detInvertibleOfInvertible A
  convert (rfl : _ = ⅟ A.det)

Determinant of Inverse Equals Inverse of Determinant

Informal description

For any invertible square matrix $A$ over a ring $R$ with invertible determinant, the determinant of the inverse matrix $\text{⅟}A$ is equal to the inverse of the determinant of $A$, i.e., $\det(\text{⅟}A) = \text{⅟}(\det A)$.

Matrix.invertibleEquivDetInvertible definition

: Invertible A ≃ Invertible A.det

Full source

/-- Together `Matrix.detInvertibleOfInvertible` and `Matrix.invertibleOfDetInvertible` form an
equivalence, although both sides of the equiv are subsingleton anyway. -/
@[simps]
def invertibleEquivDetInvertible : InvertibleInvertible A ≃ Invertible A.det where
  toFun := @detInvertibleOfInvertible _ _ _ _ _ A
  invFun := @invertibleOfDetInvertible _ _ _ _ _ A
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence between matrix invertibility and determinant invertibility

Informal description

The equivalence between the invertibility of a square matrix $ A $ and the invertibility of its determinant $\det A$. Specifically, the function `Matrix.detInvertibleOfInvertible` maps an invertible matrix to an invertible determinant, while `Matrix.invertibleOfDetInvertible` maps an invertible determinant back to an invertible matrix. These two functions form a bijection, although both sides of the equivalence are subsingleton types (i.e., any two instances are equal).

Matrix.unitOfDetInvertible definition

[Invertible A.det] : (Matrix n n α)ˣ

Full source

/-- Given a proof that `A.det` has a constructive inverse, lift `A` to `(Matrix n n α)ˣ` -/
def unitOfDetInvertible [Invertible A.det] : (Matrix n n α)ˣ :=
  @unitOfInvertible _ _ A (invertibleOfDetInvertible A)

Unit matrix from invertible determinant

Informal description

Given a square matrix $A$ of size $n \times n$ over a ring $\alpha$ such that its determinant $\det A$ is invertible, the function `Matrix.unitOfDetInvertible` constructs the unit (invertible element) associated with $A$ in the monoid of matrices, where the underlying element is $A$ itself and its inverse is constructed from the inverse of the determinant.

Matrix.isUnit_iff_isUnit_det theorem

: IsUnit A ↔ IsUnit A.det

Full source

/-- When lowered to a prop, `Matrix.invertibleEquivDetInvertible` forms an `iff`. -/
theorem isUnit_iff_isUnit_det : IsUnitIsUnit A ↔ IsUnit A.det := by
  simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr]

Matrix Invertibility Criterion via Determinant: $\text{IsUnit}(A) \leftrightarrow \text{IsUnit}(\det A)$

Informal description

A square matrix $A$ over a ring $R$ is invertible if and only if its determinant $\det(A)$ is a unit in $R$.

Matrix.isUnits_det_units theorem

(A : (Matrix n n α)ˣ) : IsUnit (A : Matrix n n α).det

Full source

@[simp]
theorem isUnits_det_units (A : (Matrix n n α)ˣ) : IsUnit (A : Matrix n n α).det :=
  isUnit_iff_isUnit_det _ |>.mp A.isUnit

Determinant of Invertible Matrix is Unit

Informal description

For any invertible square matrix $A$ of size $n \times n$ over a ring $\alpha$, the determinant of $A$ is a unit in $\alpha$.

Matrix.isUnit_det_of_invertible theorem

[Invertible A] : IsUnit A.det

Full source

theorem isUnit_det_of_invertible [Invertible A] : IsUnit A.det :=
  @isUnit_of_invertible _ _ _ (detInvertibleOfInvertible A)

Invertible Matrix has Unit Determinant

Informal description

For any square matrix $A$ over a ring $R$, if $A$ is invertible, then its determinant $\det(A)$ is a unit in $R$.

Matrix.isUnit_det_of_left_inverse theorem

(h : B * A = 1) : IsUnit A.det

Full source

theorem isUnit_det_of_left_inverse (h : B * A = 1) : IsUnit A.det :=
  @isUnit_of_invertible _ _ _ (detInvertibleOfLeftInverse _ _ h)

Determinant is Unit Given Left Inverse

Informal description

For any square matrices $A$ and $B$ over a ring $R$, if $BA = I$ (the identity matrix), then the determinant of $A$ is a unit in $R$.

Matrix.isUnit_det_of_right_inverse theorem

(h : A * B = 1) : IsUnit A.det

Full source

theorem isUnit_det_of_right_inverse (h : A * B = 1) : IsUnit A.det :=
  @isUnit_of_invertible _ _ _ (detInvertibleOfRightInverse _ _ h)

Determinant is Unit for Matrices with Right Inverse

Informal description

For square matrices $A$ and $B$ over a ring $R$, if $A$ has a right inverse (i.e., $AB = I$), then the determinant of $A$ is a unit in $R$.

Matrix.det_ne_zero_of_left_inverse theorem

[Nontrivial α] (h : B * A = 1) : A.det ≠ 0

Full source

theorem det_ne_zero_of_left_inverse [Nontrivial α] (h : B * A = 1) : A.det ≠ 0 :=
  (isUnit_det_of_left_inverse h).ne_zero

Nonzero Determinant for Matrices with Left Inverse

Informal description

Let $A$ and $B$ be square matrices over a nontrivial ring $\alpha$. If $B$ is a left inverse of $A$ (i.e., $BA = I$), then the determinant of $A$ is nonzero, i.e., $\det(A) \neq 0$.

Matrix.det_ne_zero_of_right_inverse theorem

[Nontrivial α] (h : A * B = 1) : A.det ≠ 0

Full source

theorem det_ne_zero_of_right_inverse [Nontrivial α] (h : A * B = 1) : A.det ≠ 0 :=
  (isUnit_det_of_right_inverse h).ne_zero

Nonzero Determinant for Matrices with Right Inverse

Informal description

Let $A$ and $B$ be square matrices over a nontrivial ring $\alpha$. If $A$ has a right inverse (i.e., $AB = I$), then the determinant of $A$ is nonzero.

Matrix.isUnit_det_transpose theorem

(h : IsUnit A.det) : IsUnit Aᵀ.det

Full source

theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det := by
  rw [det_transpose]
  exact h

Transpose Preserves Unit Determinant

Informal description

For any square matrix $A$ of size $n \times n$ over a ring, if the determinant of $A$ is a unit in the ring, then the determinant of the transpose matrix $A^\top$ is also a unit.

Matrix.inv instance

: Inv (Matrix n n α)

Full source

/-- The inverse of a square matrix, when it is invertible (and zero otherwise). -/
noncomputable instance inv : Inv (Matrix n n α) :=
  ⟨fun A => Ring.inverse A.det • A.adjugate⟩

Matrix Inverse via Adjugate and Determinant

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $\alpha$, the inverse $A^{-1}$ is defined as the scalar multiplication of the ring inverse of the determinant of $A$ (if it exists) with the adjugate matrix of $A$. If the determinant is not invertible, the inverse is defined to be the zero matrix.

Matrix.inv_def theorem

(A : Matrix n n α) : A⁻¹ = Ring.inverse A.det • A.adjugate

Full source

theorem inv_def (A : Matrix n n α) : A⁻¹ = Ring.inverse A.det • A.adjugate :=
  rfl

Matrix Inverse via Adjugate and Determinant

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $\alpha$, the inverse $A^{-1}$ is equal to the scalar multiplication of the ring inverse of the determinant of $A$ with the adjugate matrix of $A$, i.e., $A^{-1} = (\det A)^{-1} \cdot \text{adj}(A)$.

Matrix.nonsing_inv_apply_not_isUnit theorem

(h : ¬IsUnit A.det) : A⁻¹ = 0

Full source

theorem nonsing_inv_apply_not_isUnit (h : ¬IsUnit A.det) : A⁻¹ = 0 := by
  rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]

Inverse of Non-Unit Determinant Matrix is Zero

Informal description

For any square matrix $A$ over a ring, if the determinant of $A$ is not a unit, then the inverse $A^{-1}$ is the zero matrix.

Matrix.nonsing_inv_apply theorem

(h : IsUnit A.det) : A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate

Full source

theorem nonsing_inv_apply (h : IsUnit A.det) : A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate := by
  rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]

Inverse Matrix Formula for Units via Adjugate and Determinant

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $\alpha$, if the determinant $\det A$ is a unit in $\alpha$, then the inverse matrix $A^{-1}$ is given by the scalar multiplication of the inverse of the unit $\det A$ with the adjugate matrix of $A$, i.e., \[ A^{-1} = (\det A)^{-1} \cdot \text{adj}(A). \]

Matrix.invOf_eq_nonsing_inv theorem

[Invertible A] : ⅟ A = A⁻¹

Full source

/-- The nonsingular inverse is the same as `invOf` when `A` is invertible. -/
@[simp]
theorem invOf_eq_nonsing_inv [Invertible A] : ⅟ A = A⁻¹ := by
  letI := detInvertibleOfInvertible A
  rw [inv_def, Ring.inverse_invertible, invOf_eq]

Invertible Matrix Inverse Equals Nonsingular Inverse

Informal description

For any invertible square matrix $A$ over a ring, the inverse $\text{⅟}A$ is equal to the nonsingular inverse $A^{-1}$.

Matrix.coe_units_inv theorem

(A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α)

Full source

/-- Coercing the result of `Units.instInv` is the same as coercing first and applying the
nonsingular inverse. -/
@[simp, norm_cast]
theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α) := by
  letI := A.invertible
  rw [← invOf_eq_nonsing_inv, invOf_units]

Coercion of Group Inverse Equals Matrix Inverse for Invertible Matrices

Informal description

For any invertible square matrix $A$ of size $n \times n$ over a ring $\alpha$, the inverse of $A$ in the group of units (denoted by $A^{-1}$) is equal to the nonsingular inverse of $A$ (also denoted by $A^{-1}$). In other words, the coercion of the group inverse equals the matrix inverse.

Matrix.nonsing_inv_eq_ringInverse theorem

: A⁻¹ = Ring.inverse A

Full source

/-- The nonsingular inverse is the same as the general `Ring.inverse`. -/
theorem nonsing_inv_eq_ringInverse : A⁻¹ = Ring.inverse A := by
  by_cases h_det : IsUnit A.det
  · cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible
    rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]
  · have h := mt A.isUnit_iff_isUnit_det.mp h_det
    rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]

Nonsingular Inverse Equals Ring Inverse: $A^{-1} = \text{Ring.inverse}(A)$

Informal description

For any square matrix $A$ over a ring, the nonsingular inverse $A^{-1}$ is equal to the ring-theoretic inverse $\text{Ring.inverse}(A)$.

Matrix.transpose_nonsing_inv theorem

: A⁻¹ᵀ = Aᵀ⁻¹

Full source

theorem transpose_nonsing_inv : A⁻¹A⁻¹ᵀ = AᵀAᵀ⁻¹ := by
  rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]

Transpose-Inverse Commutation: $(A^{-1})^\top = (A^\top)^{-1}$

Informal description

For any square matrix $A$ over a ring $\alpha$, the transpose of the inverse of $A$ is equal to the inverse of the transpose of $A$, i.e., \[ (A^{-1})^\top = (A^\top)^{-1}. \]

Matrix.conjTranspose_nonsing_inv theorem

[StarRing α] : A⁻¹ᴴ = Aᴴ⁻¹

Full source

theorem conjTranspose_nonsing_inv [StarRing α] : A⁻¹A⁻¹ᴴ = AᴴAᴴ⁻¹ := by
  rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
    Ring.inverse_star]

Conjugate Transpose-Inverse Commutation: $(A^{-1})^\dagger = (A^\dagger)^{-1}$

Informal description

For any square matrix $A$ over a ring $\alpha$ equipped with a star ring structure, the conjugate transpose of the inverse of $A$ is equal to the inverse of the conjugate transpose of $A$, i.e., \[ (A^{-1})^\dagger = (A^\dagger)^{-1}. \]

Matrix.mul_nonsing_inv theorem

(h : IsUnit A.det) : A * A⁻¹ = 1

Full source

/-- The `nonsing_inv` of `A` is a right inverse. -/
@[simp]
theorem mul_nonsing_inv (h : IsUnit A.det) : A * A⁻¹ = 1 := by
  cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
  rw [← invOf_eq_nonsing_inv, mul_invOf_self]

Right Inverse Property for Nonsingular Matrices: $A A^{-1} = I$ when $\det(A)$ is a unit

Informal description

For any square matrix $A$ over a ring $R$, if the determinant $\det(A)$ is a unit in $R$, then the product of $A$ with its nonsingular inverse $A^{-1}$ equals the identity matrix, i.e., $A A^{-1} = I$.

Matrix.nonsing_inv_mul theorem

(h : IsUnit A.det) : A⁻¹ * A = 1

Full source

/-- The `nonsing_inv` of `A` is a left inverse. -/
@[simp]
theorem nonsing_inv_mul (h : IsUnit A.det) : A⁻¹ * A = 1 := by
  cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
  rw [← invOf_eq_nonsing_inv, invOf_mul_self]

Left Inverse Property for Nonsingular Matrices: $A^{-1}A = I$

Informal description

For any square matrix $A$ over a ring $R$, if the determinant $\det(A)$ is a unit in $R$, then the product of the nonsingular inverse $A^{-1}$ and $A$ equals the identity matrix, i.e., $A^{-1}A = I$.

Matrix.instInvertibleInv instance

[Invertible A] : Invertible A⁻¹

Full source

instance [Invertible A] : Invertible A⁻¹ := by
  rw [← invOf_eq_nonsing_inv]
  infer_instance

Invertibility of Matrix Inverses

Informal description

For any square matrix $A$ over a ring $\alpha$, if $A$ is invertible, then its inverse $A^{-1}$ is also invertible.

Matrix.inv_inv_of_invertible theorem

[Invertible A] : A⁻¹⁻¹ = A

Full source

@[simp]
theorem inv_inv_of_invertible [Invertible A] : A⁻¹A⁻¹⁻¹ = A := by
  simp only [← invOf_eq_nonsing_inv, invOf_invOf]

Double Inverse Property for Invertible Matrices: $(A^{-1})^{-1} = A$

Informal description

For any invertible square matrix $A$ over a ring $\alpha$, the inverse of the inverse of $A$ is equal to $A$, i.e., $(A^{-1})^{-1} = A$.

Matrix.mul_nonsing_inv_cancel_right theorem

(B : Matrix m n α) (h : IsUnit A.det) : B * A * A⁻¹ = B

Full source

@[simp]
theorem mul_nonsing_inv_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B * A * A⁻¹ = B := by
  simp [Matrix.mul_assoc, mul_nonsing_inv A h]

Right Cancellation Property for Nonsingular Matrices: $B A A^{-1} = B$ when $\det(A)$ is a unit

Informal description

For any $m \times n$ matrix $B$ over a ring $\alpha$ and any $n \times n$ matrix $A$ over $\alpha$ such that $\det(A)$ is a unit in $\alpha$, the product $B * A * A^{-1}$ equals $B$.

Matrix.mul_nonsing_inv_cancel_left theorem

(B : Matrix n m α) (h : IsUnit A.det) : A * (A⁻¹ * B) = B

Full source

@[simp]
theorem mul_nonsing_inv_cancel_left (B : Matrix n m α) (h : IsUnit A.det) : A * (A⁻¹ * B) = B := by
  simp [← Matrix.mul_assoc, mul_nonsing_inv A h]

Left Cancellation Property for Nonsingular Matrices: $A (A^{-1} B) = B$ when $\det(A)$ is a unit

Informal description

For any $n \times m$ matrix $B$ over a ring $\alpha$, if the determinant of an $n \times n$ matrix $A$ is a unit in $\alpha$, then the product $A (A^{-1} B)$ equals $B$.

Matrix.nonsing_inv_mul_cancel_right theorem

(B : Matrix m n α) (h : IsUnit A.det) : B * A⁻¹ * A = B

Full source

@[simp]
theorem nonsing_inv_mul_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B * A⁻¹ * A = B := by
  simp [Matrix.mul_assoc, nonsing_inv_mul A h]

Right cancellation property for matrix inverse: $B A^{-1} A = B$

Informal description

For any $m \times n$ matrix $B$ over a ring $\alpha$ and any square matrix $A$ of size $n \times n$ with invertible determinant, the product $B A^{-1} A$ equals $B$.

Matrix.nonsing_inv_mul_cancel_left theorem

(B : Matrix n m α) (h : IsUnit A.det) : A⁻¹ * (A * B) = B

Full source

@[simp]
theorem nonsing_inv_mul_cancel_left (B : Matrix n m α) (h : IsUnit A.det) : A⁻¹ * (A * B) = B := by
  simp [← Matrix.mul_assoc, nonsing_inv_mul A h]

Left cancellation property for matrix inverse: $A^{-1}(AB) = B$ when $\det A$ is invertible

Informal description

For any $n \times n$ matrix $A$ over a ring $\alpha$ with invertible determinant, and any $n \times m$ matrix $B$ over $\alpha$, the following equality holds: \[ A^{-1}(AB) = B \]

Matrix.mul_inv_of_invertible theorem

[Invertible A] : A * A⁻¹ = 1

Full source

@[simp]
theorem mul_inv_of_invertible [Invertible A] : A * A⁻¹ = 1 :=
  mul_nonsing_inv A (isUnit_det_of_invertible A)

Right Inverse Property for Invertible Matrices: $A A^{-1} = I$

Informal description

For any invertible square matrix $A$ over a ring $R$, the product of $A$ with its inverse $A^{-1}$ equals the identity matrix, i.e., $A A^{-1} = I$.

Matrix.inv_mul_of_invertible theorem

[Invertible A] : A⁻¹ * A = 1

Full source

@[simp]
theorem inv_mul_of_invertible [Invertible A] : A⁻¹ * A = 1 :=
  nonsing_inv_mul A (isUnit_det_of_invertible A)

Left Inverse Property for Invertible Matrices: $A^{-1}A = I$

Informal description

For any invertible square matrix $A$ over a ring $R$, the product of its inverse $A^{-1}$ and $A$ equals the identity matrix, i.e., $A^{-1}A = I$.

Matrix.mul_inv_cancel_right_of_invertible theorem

(B : Matrix m n α) [Invertible A] : B * A * A⁻¹ = B

Full source

@[simp]
theorem mul_inv_cancel_right_of_invertible (B : Matrix m n α) [Invertible A] : B * A * A⁻¹ = B :=
  mul_nonsing_inv_cancel_right A B (isUnit_det_of_invertible A)

Right Cancellation Property for Invertible Matrices: $B A A^{-1} = B$

Informal description

For any $m \times n$ matrix $B$ over a ring $\alpha$ and any invertible $n \times n$ matrix $A$ over $\alpha$, the product $B A A^{-1}$ equals $B$.

Matrix.mul_inv_cancel_left_of_invertible theorem

(B : Matrix n m α) [Invertible A] : A * (A⁻¹ * B) = B

Full source

@[simp]
theorem mul_inv_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A * (A⁻¹ * B) = B :=
  mul_nonsing_inv_cancel_left A B (isUnit_det_of_invertible A)

Left Cancellation Property for Invertible Matrices: $A (A^{-1} B) = B$

Informal description

For any invertible $n \times n$ matrix $A$ over a ring $\alpha$ and any $n \times m$ matrix $B$ over $\alpha$, the product $A (A^{-1} B)$ equals $B$.

Matrix.inv_mul_cancel_right_of_invertible theorem

(B : Matrix m n α) [Invertible A] : B * A⁻¹ * A = B

Full source

@[simp]
theorem inv_mul_cancel_right_of_invertible (B : Matrix m n α) [Invertible A] : B * A⁻¹ * A = B :=
  nonsing_inv_mul_cancel_right A B (isUnit_det_of_invertible A)

Right cancellation property for invertible matrix inverse: $B A^{-1} A = B$

Informal description

For any $m \times n$ matrix $B$ over a ring $\alpha$ and any invertible $n \times n$ matrix $A$ over $\alpha$, the product $B A^{-1} A$ equals $B$.

Matrix.inv_mul_cancel_left_of_invertible theorem

(B : Matrix n m α) [Invertible A] : A⁻¹ * (A * B) = B

Full source

@[simp]
theorem inv_mul_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A⁻¹ * (A * B) = B :=
  nonsing_inv_mul_cancel_left A B (isUnit_det_of_invertible A)

Left cancellation property for invertible matrix multiplication: $A^{-1}(AB) = B$

Informal description

For any invertible $n \times n$ matrix $A$ over a ring $\alpha$ and any $n \times m$ matrix $B$ over $\alpha$, the following equality holds: \[ A^{-1}(AB) = B \]

Matrix.inv_mul_eq_iff_eq_mul_of_invertible theorem

(A B C : Matrix n n α) [Invertible A] : A⁻¹ * B = C ↔ B = A * C

Full source

theorem inv_mul_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] :
    A⁻¹A⁻¹ * B = C ↔ B = A * C :=
  ⟨fun h => by rw [← h, mul_inv_cancel_left_of_invertible],
   fun h => by rw [h, inv_mul_cancel_left_of_invertible]⟩

Equivalence of Inverse Matrix Multiplication: $A^{-1}B = C \leftrightarrow B = AC$ for Invertible $A$

Informal description

For any invertible $n \times n$ matrix $A$ over a ring $\alpha$ and any $n \times n$ matrices $B$ and $C$ over $\alpha$, the following equivalence holds: \[ A^{-1}B = C \quad \text{if and only if} \quad B = AC. \]

Matrix.mul_inv_eq_iff_eq_mul_of_invertible theorem

(A B C : Matrix n n α) [Invertible A] : B * A⁻¹ = C ↔ B = C * A

Full source

theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] :
    B * A⁻¹ = C ↔ B = C * A :=
  ⟨fun h => by rw [← h, inv_mul_cancel_right_of_invertible],
   fun h => by rw [h, mul_inv_cancel_right_of_invertible]⟩

Equivalence of Right Multiplication by Inverse: $B A^{-1} = C \leftrightarrow B = C A$

Informal description

For any invertible $n \times n$ matrix $A$ over a ring $\alpha$ and any $n \times n$ matrices $B$ and $C$ over $\alpha$, the equation $B A^{-1} = C$ holds if and only if $B = C A$.

Matrix.inv_mulVec_eq_vec theorem

{A : Matrix n n α} [Invertible A] {u v : n → α} (hM : u = A.mulVec v) : A⁻¹.mulVec u = v

Full source

lemma inv_mulVec_eq_vec {A : Matrix n n α} [Invertible A]
    {u v : n → α} (hM : u = A.mulVec v) : A⁻¹.mulVec u = v := by
  rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]

Inverse Matrix-Vector Product Recovers Original Vector: $A^{-1}u = v$ when $u = Av$

Informal description

Let $A$ be an invertible $n \times n$ matrix over a ring $\alpha$, and let $u, v$ be vectors in $\alpha^n$ such that $u = A v$. Then the matrix-vector product of the inverse matrix $A^{-1}$ with $u$ yields $v$, i.e., $A^{-1} u = v$.

Matrix.mul_right_injective_of_invertible theorem

[Invertible A] : Function.Injective (fun (x : Matrix n m α) => A * x)

Full source

lemma mul_right_injective_of_invertible [Invertible A] :
    Function.Injective (fun (x : Matrix n m α) => A * x) :=
  fun _ _ h => by simpa only [inv_mul_cancel_left_of_invertible] using congr_arg (A⁻¹ * ·) h

Injectivity of Left Multiplication by Invertible Matrix

Informal description

For any invertible $n \times n$ matrix $A$ over a ring $\alpha$, the left multiplication map $x \mapsto A x$ is injective on the space of $n \times m$ matrices over $\alpha$. In other words, if $A x_1 = A x_2$ for two matrices $x_1, x_2 \in \text{Matrix}\,n\,m\,\alpha$, then $x_1 = x_2$.

Matrix.mul_left_injective_of_invertible theorem

[Invertible A] : Function.Injective (fun (x : Matrix m n α) => x * A)

Full source

lemma mul_left_injective_of_invertible [Invertible A] :
    Function.Injective (fun (x : Matrix m n α) => x * A) :=
  fun a x hax => by simpa only [mul_inv_cancel_right_of_invertible] using congr_arg (· * A⁻¹) hax

Injectivity of Left Multiplication by Invertible Matrix

Informal description

For any invertible $n \times n$ matrix $A$ over a ring $\alpha$, the left multiplication map $x \mapsto x * A$ is injective on the space of $m \times n$ matrices over $\alpha$. That is, if $x * A = y * A$ for $x, y \in \text{Matrix}(m, n, \alpha)$, then $x = y$.

Matrix.mul_right_inj_of_invertible theorem

[Invertible A] {x y : Matrix n m α} : A * x = A * y ↔ x = y

Full source

lemma mul_right_inj_of_invertible [Invertible A] {x y : Matrix n m α} : A * x = A * y ↔ x = y :=
  (mul_right_injective_of_invertible A).eq_iff

Invertible Matrix Left Multiplication is Injective: $A x = A y \leftrightarrow x = y$

Informal description

For any invertible $n \times n$ matrix $A$ over a ring $\alpha$, and for any two $n \times m$ matrices $x$ and $y$ over $\alpha$, the equality $A x = A y$ holds if and only if $x = y$.

Matrix.mul_left_inj_of_invertible theorem

[Invertible A] {x y : Matrix m n α} : x * A = y * A ↔ x = y

Full source

lemma mul_left_inj_of_invertible [Invertible A] {x y : Matrix m n α} : x * A = y * A ↔ x = y :=
  (mul_left_injective_of_invertible A).eq_iff

Left Cancellation Property for Multiplication by Invertible Matrix

Informal description

For any invertible $n \times n$ matrix $A$ over a ring $\alpha$, and any two $m \times n$ matrices $x$ and $y$ over $\alpha$, the equality $x * A = y * A$ holds if and only if $x = y$.

Matrix.mul_left_injective_of_inv theorem

(A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) : Function.Injective (fun x : Matrix l m α => x * A)

Full source

lemma mul_left_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :
    Function.Injective (fun x : Matrix l m α => x * A) := fun _ _ g => by
  simpa only [Matrix.mul_assoc, Matrix.mul_one, h] using congr_arg (· * B) g

Injectivity of Left Multiplication by a Matrix with Right Inverse

Informal description

Let $A$ be an $m \times n$ matrix and $B$ an $n \times m$ matrix over a type $\alpha$ such that $A B = I_m$ (the $m \times m$ identity matrix). Then the left multiplication map $L_A : \text{Matrix}_{l \times m}(\alpha) \to \text{Matrix}_{l \times n}(\alpha)$ defined by $X \mapsto X A$ is injective.

Matrix.mul_right_injective_of_inv theorem

(A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) : Function.Injective (fun x : Matrix m l α => B * x)

Full source

lemma mul_right_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :
    Function.Injective (fun x : Matrix m l α => B * x) :=
  fun _ _ g => by simpa only [← Matrix.mul_assoc, Matrix.one_mul, h] using congr_arg (A * ·) g

Injectivity of Right Multiplication by a Matrix with Left Inverse

Informal description

Let $A$ be an $m \times n$ matrix and $B$ an $n \times m$ matrix over a type $\alpha$ such that $A B = I_m$ (the $m \times m$ identity matrix). Then the right multiplication map $R_B : \text{Matrix}_{m \times l}(\alpha) \to \text{Matrix}_{n \times l}(\alpha)$ defined by $X \mapsto B X$ is injective.

Matrix.vecMul_surjective_iff_exists_left_inverse theorem

 [DecidableEq n] [Fintype m] [Finite n] {A : Matrix m n R} :
  Function.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1

Full source

theorem vecMul_surjective_iff_exists_left_inverse
    [DecidableEq n] [Fintype m] [Finite n] {A : Matrix m n R} :
    Function.SurjectiveFunction.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1 := by
  cases nonempty_fintype n
  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩
  choose rows hrows using (h <| Pi.single · 1)
  refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩
  rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]
  rfl

Surjectivity of Matrix Vector Left Multiplication Equivalence to Left Invertibility

Informal description

Let $A$ be an $m \times n$ matrix over a ring $R$, with $m$ finite and $n$ finite or infinite. The vector left multiplication map $L_A : R^m \to R^n$ defined by $x \mapsto x^T A$ is surjective if and only if there exists an $n \times m$ matrix $B$ such that $BA = I_n$, where $I_n$ is the $n \times n$ identity matrix.

Matrix.mulVec_surjective_iff_exists_right_inverse theorem

 [DecidableEq m] [Finite m] [Fintype n] {A : Matrix m n R} :
  Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1

Full source

theorem mulVec_surjective_iff_exists_right_inverse
    [DecidableEq m] [Finite m] [Fintype n] {A : Matrix m n R} :
    Function.SurjectiveFunction.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1 := by
  cases nonempty_fintype m
  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩
  choose cols hcols using (h <| Pi.single · 1)
  refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩
  rw [one_eq_pi_single, Pi.single_comm, ← hcols j]
  rfl

Surjectivity of Matrix-Vector Multiplication is Equivalent to Existence of Right Inverse

Informal description

Let $A$ be an $m \times n$ matrix over a ring $R$, with $m$ finite and $n$ a fintype. Then the matrix-vector multiplication map $A \cdot \_ : R^n \to R^m$ is surjective if and only if there exists an $n \times m$ matrix $B$ such that $A B = I_m$, where $I_m$ is the $m \times m$ identity matrix.

Matrix.vecMul_surjective_iff_isUnit theorem

{A : Matrix m m R} : Function.Surjective A.vecMul ↔ IsUnit A

Full source

theorem vecMul_surjective_iff_isUnit {A : Matrix m m R} :
    Function.SurjectiveFunction.Surjective A.vecMul ↔ IsUnit A := by
  rw [vecMul_surjective_iff_exists_left_inverse, exists_left_inverse_iff_isUnit]

Surjectivity of Matrix Vector Left Multiplication is Equivalent to Matrix Being a Unit

Informal description

For a square matrix $A$ of size $m \times m$ over a ring $R$, the vector left multiplication map $L_A : R^m \to R^m$ defined by $x \mapsto x^T A$ is surjective if and only if $A$ is a unit in the matrix ring (i.e., $A$ has a multiplicative inverse).

Matrix.mulVec_surjective_iff_isUnit theorem

{A : Matrix m m R} : Function.Surjective A.mulVec ↔ IsUnit A

Full source

theorem mulVec_surjective_iff_isUnit {A : Matrix m m R} :
    Function.SurjectiveFunction.Surjective A.mulVec ↔ IsUnit A := by
  rw [mulVec_surjective_iff_exists_right_inverse, exists_right_inverse_iff_isUnit]

Surjectivity of Matrix-Vector Multiplication is Equivalent to Matrix Being a Unit

Informal description

For a square matrix $A$ of size $m \times m$ over a ring $R$, the matrix-vector multiplication map $A \cdot \_ : R^m \to R^m$ is surjective if and only if $A$ is a unit in the ring of matrices (i.e., $A$ has a multiplicative inverse).

Matrix.vecMul_injective_iff_isUnit theorem

{A : Matrix m m K} : Function.Injective A.vecMul ↔ IsUnit A

Full source

theorem vecMul_injective_iff_isUnit {A : Matrix m m K} :
    Function.InjectiveFunction.Injective A.vecMul ↔ IsUnit A := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← vecMul_surjective_iff_isUnit]
    exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h
  change Function.Injective A.vecMulLinear
  rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
  intro c hc
  replace h := h.invertible
  simpa using congr_arg A⁻¹.vecMulLinear hc

Injectivity of Vector-Matrix Multiplication is Equivalent to Matrix Invertibility

Informal description

For a square matrix $A$ of size $m \times m$ over a division ring $K$, the vector left multiplication map $x \mapsto x^T A$ is injective if and only if $A$ is invertible (i.e., $A$ has a multiplicative inverse in the matrix ring).

Matrix.mulVec_injective_iff_isUnit theorem

{A : Matrix m m K} : Function.Injective A.mulVec ↔ IsUnit A

Full source

theorem mulVec_injective_iff_isUnit {A : Matrix m m K} :
    Function.InjectiveFunction.Injective A.mulVec ↔ IsUnit A := by
  rw [← isUnit_transpose, ← vecMul_injective_iff_isUnit]
  simp_rw [vecMul_transpose]

Injectivity of Matrix-Vector Multiplication is Equivalent to Matrix Invertibility

Informal description

For a square matrix $A$ of size $m \times m$ over a division ring $K$, the matrix-vector multiplication map $A \cdot \_ : K^m \to K^m$ is injective if and only if $A$ is invertible (i.e., $A$ has a multiplicative inverse in the matrix ring).

Matrix.linearIndependent_rows_iff_isUnit theorem

{A : Matrix m m K} : LinearIndependent K A.row ↔ IsUnit A

Full source

theorem linearIndependent_rows_iff_isUnit {A : Matrix m m K} :
    LinearIndependentLinearIndependent K A.row ↔ IsUnit A := by
  rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
    ← vecMul_injective_iff_isUnit, coe_vecMulLinear]

Linear Independence of Rows is Equivalent to Matrix Invertibility

Informal description

For a square matrix $A$ of size $m \times m$ over a division ring $K$, the rows of $A$ are linearly independent over $K$ if and only if $A$ is invertible (i.e., $A$ has a multiplicative inverse in the matrix ring).

Matrix.linearIndependent_cols_iff_isUnit theorem

{A : Matrix m m K} : LinearIndependent K A.col ↔ IsUnit A

Full source

theorem linearIndependent_cols_iff_isUnit {A : Matrix m m K} :
    LinearIndependentLinearIndependent K A.col ↔ IsUnit A := by
  rw [← row_transpose, linearIndependent_rows_iff_isUnit, isUnit_transpose]

Linear Independence of Columns is Equivalent to Matrix Invertibility

Informal description

For a square matrix $A$ of size $m \times m$ over a division ring $K$, the columns of $A$ are linearly independent over $K$ if and only if $A$ is invertible (i.e., $A$ has a multiplicative inverse in the matrix ring).

Matrix.vecMul_surjective_of_invertible theorem

(A : Matrix m m R) [Invertible A] : Function.Surjective A.vecMul

Full source

theorem vecMul_surjective_of_invertible (A : Matrix m m R) [Invertible A] :
    Function.Surjective A.vecMul :=
  vecMul_surjective_iff_isUnit.2 <| isUnit_of_invertible A

Surjectivity of Left Vector Multiplication by an Invertible Matrix

Informal description

For any invertible square matrix $A$ of size $m \times m$ over a ring $R$, the left vector multiplication map $x \mapsto x^T A$ is surjective.

Matrix.mulVec_surjective_of_invertible theorem

(A : Matrix m m R) [Invertible A] : Function.Surjective A.mulVec

Full source

theorem mulVec_surjective_of_invertible (A : Matrix m m R) [Invertible A] :
    Function.Surjective A.mulVec :=
  mulVec_surjective_iff_isUnit.2 <| isUnit_of_invertible A

Surjectivity of Matrix-Vector Multiplication for Invertible Matrices

Informal description

For any square matrix $A$ of size $m \times m$ over a ring $R$, if $A$ is invertible, then the matrix-vector multiplication map $A \cdot \_ : R^m \to R^m$ is surjective.

Matrix.vecMul_injective_of_invertible theorem

(A : Matrix m m K) [Invertible A] : Function.Injective A.vecMul

Full source

theorem vecMul_injective_of_invertible (A : Matrix m m K) [Invertible A] :
    Function.Injective A.vecMul :=
  vecMul_injective_iff_isUnit.2 <| isUnit_of_invertible A

Injectivity of Left Vector Multiplication by Invertible Matrix

Informal description

For any invertible square matrix $A$ of size $m \times m$ over a division ring $K$, the left vector multiplication map $x \mapsto x^T A$ is injective.

Matrix.mulVec_injective_of_invertible theorem

(A : Matrix m m K) [Invertible A] : Function.Injective A.mulVec

Full source

theorem mulVec_injective_of_invertible (A : Matrix m m K) [Invertible A] :
    Function.Injective A.mulVec :=
  mulVec_injective_iff_isUnit.2 <| isUnit_of_invertible A

Injectivity of Matrix-Vector Multiplication for Invertible Matrices

Informal description

For any invertible square matrix $A$ of size $m \times m$ over a division ring $K$, the matrix-vector multiplication map $v \mapsto A \cdot v$ is injective.

Matrix.linearIndependent_rows_of_invertible theorem

(A : Matrix m m K) [Invertible A] : LinearIndependent K A.row

Full source

theorem linearIndependent_rows_of_invertible (A : Matrix m m K) [Invertible A] :
    LinearIndependent K A.row :=
  linearIndependent_rows_iff_isUnit.2 <| isUnit_of_invertible A

Linear Independence of Rows for Invertible Matrices

Informal description

For any invertible square matrix $A$ of size $m \times m$ over a division ring $K$, the rows of $A$ are linearly independent over $K$.

Matrix.linearIndependent_cols_of_invertible theorem

(A : Matrix m m K) [Invertible A] : LinearIndependent K A.col

Full source

theorem linearIndependent_cols_of_invertible (A : Matrix m m K) [Invertible A] :
    LinearIndependent K A.col :=
  linearIndependent_cols_iff_isUnit.2 <| isUnit_of_invertible A

Linear Independence of Columns for Invertible Matrices

Informal description

For any invertible square matrix $A$ of size $m \times m$ over a division ring $K$, the columns of $A$ are linearly independent over $K$.

Matrix.nonsing_inv_cancel_or_zero theorem

: A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Full source

theorem nonsing_inv_cancel_or_zero : A⁻¹A⁻¹ * A = 1 ∧ A * A⁻¹ = 1A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0 := by
  by_cases h : IsUnit A.det
  · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩
  · exact Or.inr (nonsing_inv_apply_not_isUnit _ h)

Inverse Cancellation or Zero Property for Square Matrices

Informal description

For any square matrix $A$ over a ring, either the inverse $A^{-1}$ satisfies both $A^{-1}A = I$ and $AA^{-1} = I$ (where $I$ is the identity matrix), or $A^{-1}$ is the zero matrix.

Matrix.det_nonsing_inv_mul_det theorem

(h : IsUnit A.det) : A⁻¹.det * A.det = 1

Full source

theorem det_nonsing_inv_mul_det (h : IsUnit A.det) : A⁻¹.det * A.det = 1 := by
  rw [← det_mul, A.nonsing_inv_mul h, det_one]

Determinant of Inverse Matrix: $\det(A^{-1})\det(A) = 1$ when $\det(A)$ is invertible

Informal description

For any square matrix $A$ over a ring $R$, if the determinant $\det(A)$ is a unit in $R$, then the product of the determinant of the inverse matrix $A^{-1}$ and $\det(A)$ equals $1$, i.e., \[ \det(A^{-1}) \cdot \det(A) = 1. \]

Matrix.det_nonsing_inv theorem

: A⁻¹.det = Ring.inverse A.det

Full source

@[simp]
theorem det_nonsing_inv : A⁻¹.det = Ring.inverse A.det := by
  by_cases h : IsUnit A.det
  · cases h.nonempty_invertible
    letI := invertibleOfDetInvertible A
    rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
  cases isEmpty_or_nonempty n
  · rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
  · rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]

Determinant of Inverse Matrix Equals Ring Inverse of Determinant

Informal description

For any square matrix $A$ over a ring, the determinant of the inverse matrix $A^{-1}$ is equal to the ring inverse of the determinant of $A$, i.e., $\det(A^{-1}) = (\det A)^{-1}$.

Matrix.isUnit_nonsing_inv_det theorem

(h : IsUnit A.det) : IsUnit A⁻¹.det

Full source

theorem isUnit_nonsing_inv_det (h : IsUnit A.det) : IsUnit A⁻¹.det :=
  isUnit_of_mul_eq_one _ _ (A.det_nonsing_inv_mul_det h)

Inverse Matrix Has Unit Determinant When Original Does

Informal description

For any square matrix $A$ over a ring, if the determinant $\det(A)$ is a unit, then the determinant of the inverse matrix $\det(A^{-1})$ is also a unit.

Matrix.nonsing_inv_nonsing_inv theorem

(h : IsUnit A.det) : A⁻¹⁻¹ = A

Full source

@[simp]
theorem nonsing_inv_nonsing_inv (h : IsUnit A.det) : A⁻¹A⁻¹⁻¹ = A :=
  calc
    A⁻¹A⁻¹⁻¹ = 1 * A⁻¹A⁻¹⁻¹ := by rw [Matrix.one_mul]
    _ = A * A⁻¹ * A⁻¹A⁻¹⁻¹ := by rw [A.mul_nonsing_inv h]
    _ = A := by
      rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one]

Double Inverse of Matrix Equals Original When Determinant is Unit

Informal description

For any square matrix $A$ over a ring, if the determinant $\det(A)$ is a unit, then the inverse of the inverse matrix equals the original matrix, i.e., $(A^{-1})^{-1} = A$.

Matrix.isUnit_nonsing_inv_det_iff theorem

{A : Matrix n n α} : IsUnit A⁻¹.det ↔ IsUnit A.det

Full source

theorem isUnit_nonsing_inv_det_iff {A : Matrix n n α} : IsUnitIsUnit A⁻¹.det ↔ IsUnit A.det := by
  rw [Matrix.det_nonsing_inv, isUnit_ringInverse]

Unit Determinant Criterion for Matrix Invertibility: $\det(A^{-1})$ is a unit iff $\det(A)$ is a unit

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $\alpha$, the determinant of the inverse matrix $A^{-1}$ is a unit in $\alpha$ if and only if the determinant of $A$ is a unit in $\alpha$.

Matrix.isUnit_nonsing_inv_iff theorem

{A : Matrix n n α} : IsUnit A⁻¹ ↔ IsUnit A

Full source

@[simp]
theorem isUnit_nonsing_inv_iff {A : Matrix n n α} : IsUnitIsUnit A⁻¹ ↔ IsUnit A := by
  simp_rw [isUnit_iff_isUnit_det, isUnit_nonsing_inv_det_iff]

Invertibility of Matrix Inverse: $A^{-1}$ is invertible iff $A$ is invertible

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $\alpha$, the matrix $A^{-1}$ is invertible if and only if $A$ is invertible.

Matrix.invertibleOfIsUnitDet definition

(h : IsUnit A.det) : Invertible A

Full source

/-- A version of `Matrix.invertibleOfDetInvertible` with the inverse defeq to `A⁻¹` that is
therefore noncomputable. -/
noncomputable def invertibleOfIsUnitDet (h : IsUnit A.det) : Invertible A :=
  ⟨A⁻¹, nonsing_inv_mul A h, mul_nonsing_inv A h⟩

Invertibility of matrix with unit determinant

Informal description

Given a square matrix $A$ of size $n \times n$ over a ring $\alpha$, if the determinant $\det(A)$ is a unit in $\alpha$, then $A$ is invertible. The inverse is defined as the matrix adjugate divided by the determinant, satisfying both left and right inverse properties: $A^{-1}A = I$ and $AA^{-1} = I$.

Matrix.nonsingInvUnit definition

(h : IsUnit A.det) : (Matrix n n α)ˣ

Full source

/-- A version of `Matrix.unitOfDetInvertible` with the inverse defeq to `A⁻¹` that is therefore
noncomputable. -/
noncomputable def nonsingInvUnit (h : IsUnit A.det) : (Matrix n n α)ˣ :=
  @unitOfInvertible _ _ _ (invertibleOfIsUnitDet A h)

Unit associated with an invertible matrix via its inverse

Informal description

Given a square matrix $A$ of size $n \times n$ over a ring $\alpha$, if the determinant $\det(A)$ is a unit in $\alpha$, then the function `Matrix.nonsingInvUnit` constructs the unit (invertible element) associated with $A$, where the underlying element is $A$ itself and its inverse is the explicitly given inverse $A^{-1}$ (defined as the adjugate matrix divided by the determinant).

Matrix.unitOfDetInvertible_eq_nonsingInvUnit theorem

[Invertible A.det] : unitOfDetInvertible A = nonsingInvUnit A (isUnit_of_invertible _)

Full source

theorem unitOfDetInvertible_eq_nonsingInvUnit [Invertible A.det] :
    unitOfDetInvertible A = nonsingInvUnit A (isUnit_of_invertible _) := by
  ext
  rfl

Equality of Unit Matrix Constructions via Invertible Determinant and Nonsingular Inverse

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $\alpha$ with an invertible determinant, the unit matrix constructed from $A$ via its invertible determinant equals the unit matrix constructed from $A$ via its nonsingular inverse.

Matrix.inv_eq_left_inv theorem

(h : B * A = 1) : A⁻¹ = B

Full source

/-- If matrix A is left invertible, then its inverse equals its left inverse. -/
theorem inv_eq_left_inv (h : B * A = 1) : A⁻¹ = B :=
  letI := invertibleOfLeftInverse _ _ h
  invOf_eq_nonsing_inv A ▸ invOf_eq_left_inv h

Matrix inverse equals left inverse when $BA = I$

Informal description

For any square matrices $A$ and $B$ over a ring, if $B$ is a left inverse of $A$ (i.e., $BA = I$), then the inverse $A^{-1}$ equals $B$.

Matrix.inv_eq_right_inv theorem

(h : A * B = 1) : A⁻¹ = B

Full source

/-- If matrix A is right invertible, then its inverse equals its right inverse. -/
theorem inv_eq_right_inv (h : A * B = 1) : A⁻¹ = B :=
  inv_eq_left_inv (mul_eq_one_comm.2 h)

Matrix inverse equals right inverse when $AB = I$

Informal description

For any square matrices $A$ and $B$ over a ring, if $B$ is a right inverse of $A$ (i.e., $AB = I$), then the inverse $A^{-1}$ equals $B$.

Matrix.left_inv_eq_left_inv theorem

(h : B * A = 1) (g : C * A = 1) : B = C

Full source

/-- The left inverse of matrix A is unique when existing. -/
theorem left_inv_eq_left_inv (h : B * A = 1) (g : C * A = 1) : B = C := by
  rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]

Uniqueness of Left Inverse for Square Matrices

Informal description

For any square matrices $A$, $B$, and $C$ over a ring, if both $B$ and $C$ are left inverses of $A$ (i.e., $BA = I$ and $CA = I$), then $B = C$.

Matrix.right_inv_eq_right_inv theorem

(h : A * B = 1) (g : A * C = 1) : B = C

Full source

/-- The right inverse of matrix A is unique when existing. -/
theorem right_inv_eq_right_inv (h : A * B = 1) (g : A * C = 1) : B = C := by
  rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]

Uniqueness of Right Inverse for Square Matrices

Informal description

For any square matrices $A$, $B$, and $C$ over a ring, if both $B$ and $C$ are right inverses of $A$ (i.e., $AB = I$ and $AC = I$), then $B = C$.

Matrix.right_inv_eq_left_inv theorem

(h : A * B = 1) (g : C * A = 1) : B = C

Full source

/-- The right inverse of matrix A equals the left inverse of A when they exist. -/
theorem right_inv_eq_left_inv (h : A * B = 1) (g : C * A = 1) : B = C := by
  rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]

Right Inverse Equals Left Inverse for Square Matrices

Informal description

For any square matrices $A$, $B$, and $C$ over a ring, if $B$ is a right inverse of $A$ (i.e., $AB = I$) and $C$ is a left inverse of $A$ (i.e., $CA = I$), then $B = C$.

Matrix.inv_inj theorem

(h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B

Full source

theorem inv_inj (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B := by
  refine left_inv_eq_left_inv (mul_nonsing_inv _ h') ?_
  rw [h]
  refine mul_nonsing_inv _ ?_
  rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]

Inverse Equality Implies Matrix Equality when Determinant is a Unit

Informal description

For any square matrices $A$ and $B$ over a ring, if their inverses are equal (i.e., $A^{-1} = B^{-1}$) and the determinant of $A$ is a unit, then $A = B$.

Matrix.inv_zero theorem

: (0 : Matrix n n α)⁻¹ = 0

Full source

@[simp]
theorem inv_zero : (0 : Matrix n n α)⁻¹ = 0 := by
  rcases subsingleton_or_nontrivial α with ht | ht
  · simp [eq_iff_true_of_subsingleton]
  rcases (Fintype.card n).zero_le.eq_or_lt with hc | hc
  · rw [eq_comm, Fintype.card_eq_zero_iff] at hc
    haveI := hc
    ext i
    exact (IsEmpty.false i).elim
  · have hn : Nonempty n := Fintype.card_pos_iff.mp hc
    refine nonsing_inv_apply_not_isUnit _ ?_
    simp [hn]

Inverse of Zero Matrix is Zero

Informal description

The inverse of the zero matrix (of any size $n \times n$ over any ring $\alpha$) is equal to the zero matrix, i.e., $0^{-1} = 0$.

Matrix.instInvOneClass instance

: InvOneClass (Matrix n n α)

Full source

noncomputable instance : InvOneClass (Matrix n n α) :=
  { Matrix.one, Matrix.inv with inv_one := inv_eq_left_inv (by simp) }

Square Matrices as a Ring with Inversion and Identity

Informal description

For any type `n` and any ring `α` with a multiplicative identity, the ring of square matrices of size `n × n` over `α` forms an `InvOneClass`, meaning it has both an inversion operation and a multiplicative identity (the identity matrix). The inversion operation is defined via the adjugate matrix and determinant, while the multiplicative identity is the identity matrix with ones on the diagonal and zeros elsewhere.

Matrix.inv_smul theorem

(k : α) [Invertible k] (h : IsUnit A.det) : (k • A)⁻¹ = ⅟ k • A⁻¹

Full source

theorem inv_smul (k : α) [Invertible k] (h : IsUnit A.det) : (k • A)⁻¹ = ⅟ k • A⁻¹ :=
  inv_eq_left_inv (by simp [h, smul_smul])

Inverse of Scalar Multiple: $(kA)^{-1} = ⅟k \cdot A^{-1}$

Informal description

For any scalar $k$ in a ring $\alpha$ where $k$ is invertible, and for any square matrix $A$ over $\alpha$ with invertible determinant, the inverse of the scalar multiple $kA$ is equal to the scalar multiple of the inverse of $k$ and the inverse of $A$, i.e., $(kA)^{-1} = ⅟k \cdot A^{-1}$.

Matrix.inv_smul' theorem

(k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A⁻¹

Full source

theorem inv_smul' (k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A⁻¹ :=
  inv_eq_left_inv (by simp [h, smul_smul])

Inverse of Scalar Multiple of Matrix: $(k \cdot A)^{-1} = k^{-1} \cdot A^{-1}$

Informal description

For any unit $k$ in the ring $\alpha$ and any square matrix $A$ over $\alpha$ with invertible determinant, the inverse of the scalar multiple $k \cdot A$ is equal to the scalar multiple of the inverse of $k$ with the inverse of $A$, i.e., $(k \cdot A)^{-1} = k^{-1} \cdot A^{-1}$.

Matrix.inv_adjugate theorem

(A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.unit⁻¹ • A

Full source

theorem inv_adjugate (A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.unit⁻¹ • A := by
  refine inv_eq_left_inv ?_
  rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]

Inverse of Adjugate Matrix Formula: $(\text{adjugate } A)^{-1} = (\det A)^{-1} A$

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $\alpha$, if the determinant $\det A$ is a unit, then the inverse of the adjugate matrix of $A$ is equal to the scalar multiplication of the inverse of the unit $\det A$ with $A$. That is, $$(\text{adjugate } A)^{-1} = (\det A)^{-1} \cdot A$$

Matrix.diagonalInvertible definition

{α} [NonAssocSemiring α] (v : n → α) [Invertible v] : Invertible (diagonal v)

Full source

/-- `diagonal v` is invertible if `v` is -/
def diagonalInvertible {α} [NonAssocSemiring α] (v : n → α) [Invertible v] :
    Invertible (diagonal v) :=
  Invertible.map (diagonalRingHom n α) v

Invertibility of diagonal matrix with invertible entries

Informal description

Given a non-associative semiring $\alpha$ and a vector $v : n \to \alpha$ whose components are invertible, the diagonal matrix $\text{diagonal}(v)$ is invertible. The inverse is constructed by applying the inverse operation component-wise to the vector $v$.

Matrix.invOf_diagonal_eq theorem

{α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] : ⅟ (diagonal v) = diagonal (⅟ v)

Full source

theorem invOf_diagonal_eq {α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] :
    ⅟ (diagonal v) = diagonal (⅟ v) := by
  rw [@Invertible.congr _ _ _ _ _ (diagonalInvertible v) rfl]
  rfl

Inverse of Diagonal Matrix Equals Diagonal of Inverses

Informal description

Let $\alpha$ be a semiring and $v : n \to \alpha$ be a vector of invertible elements. If the diagonal matrix $\text{diagonal}(v)$ is invertible, then its inverse is given by the diagonal matrix formed from the inverses of the elements of $v$, i.e., $\text{⅟}(\text{diagonal}(v)) = \text{diagonal}(\text{⅟}v)$.

Matrix.invertibleOfDiagonalInvertible definition

(v : n → α) [Invertible (diagonal v)] : Invertible v

Full source

/-- `v` is invertible if `diagonal v` is -/
def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : Invertible v where
  invOf := diag (⅟ (diagonal v))
  invOf_mul_self :=
    funext fun i => by
      letI : Invertible (diagonal v).det := detInvertibleOfInvertible _
      rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
      dsimp
      rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal]
      exact mul_invOf_self _
  mul_invOf_self :=
    funext fun i => by
      letI : Invertible (diagonal v).det := detInvertibleOfInvertible _
      rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
      dsimp
      rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]
      exact mul_invOf_self _

Invertibility of a vector from invertibility of its diagonal matrix

Informal description

Given a vector $ v : n \to \alpha $ such that the diagonal matrix $ \text{diagonal}(v) $ is invertible, the vector $ v $ itself is invertible. The inverse of $ v $ is obtained by taking the diagonal of the inverse of the diagonal matrix $ \text{diagonal}(v) $.

Matrix.diagonalInvertibleEquivInvertible definition

(v : n → α) : Invertible (diagonal v) ≃ Invertible v

Full source

/-- Together `Matrix.diagonalInvertible` and `Matrix.invertibleOfDiagonalInvertible` form an
equivalence, although both sides of the equiv are subsingleton anyway. -/
@[simps]
def diagonalInvertibleEquivInvertible (v : n → α) : InvertibleInvertible (diagonal v) ≃ Invertible v where
  toFun := @invertibleOfDiagonalInvertible _ _ _ _ _ _
  invFun := @diagonalInvertible _ _ _ _ _ _
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence between invertibility of diagonal matrix and its diagonal entries

Informal description

The equivalence between the invertibility of a diagonal matrix $\text{diagonal}(v)$ and the invertibility of its diagonal entries $v : n \to \alpha$. Specifically, this establishes a bijection between the structures `Invertible (diagonal v)` and `Invertible v`.

Matrix.isUnit_diagonal theorem

{v : n → α} : IsUnit (diagonal v) ↔ IsUnit v

Full source

/-- When lowered to a prop, `Matrix.diagonalInvertibleEquivInvertible` forms an `iff`. -/
@[simp]
theorem isUnit_diagonal {v : n → α} : IsUnitIsUnit (diagonal v) ↔ IsUnit v := by
  simp only [← nonempty_invertible_iff_isUnit,
    (diagonalInvertibleEquivInvertible v).nonempty_congr]

Diagonal Matrix is Unit if and only if Diagonal Entries are Units

Informal description

For a diagonal matrix $\text{diagonal}(v)$ with entries $v : n \to \alpha$, the matrix is a unit (i.e., invertible) if and only if all its diagonal entries $v$ are units.

Matrix.inv_diagonal theorem

(v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v)

Full source

theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v) := by
  rw [nonsing_inv_eq_ringInverse]
  by_cases h : IsUnit v
  · have := isUnit_diagonal.mpr h
    cases this.nonempty_invertible
    cases h.nonempty_invertible
    rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]
  · have := isUnit_diagonal.not.mpr h
    rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]

Inverse of Diagonal Matrix is Diagonal of Ring Inverses: $(\text{diag}(v))^{-1} = \text{diag}(v^{-1})$

Informal description

For any diagonal matrix $\text{diagonal}(v)$ with entries $v : n \to \alpha$, the inverse matrix $(\text{diagonal}(v))^{-1}$ is equal to the diagonal matrix formed by applying the ring inverse to each entry of $v$, i.e., $\text{diagonal}(\text{Ring.inverse}(v))$.

Matrix.inv_subsingleton theorem

[Subsingleton m] [Fintype m] [DecidableEq m] (A : Matrix m m α) : A⁻¹ = diagonal fun i => Ring.inverse (A i i)

Full source

/-- 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 `⁻¹`.
-/
@[simp]
theorem inv_subsingleton [Subsingleton m] [Fintype m] [DecidableEq m] (A : Matrix m m α) :
    A⁻¹ = diagonal fun i => Ring.inverse (A i i) := by
  rw [inv_def, adjugate_subsingleton, smul_one_eq_diagonal]
  congr! with i
  exact det_eq_elem_of_subsingleton _ _

Inverse of Subsingleton Matrix is Diagonal of Ring Inverses

Informal description

For any square matrix $A$ of size $m \times m$ over a ring $\alpha$, where the index type $m$ has at most one element (i.e., $m$ is a subsingleton type), the inverse $A^{-1}$ is equal to the diagonal matrix whose entry is the ring inverse of the diagonal entry of $A$. Specifically, for any index $i$, the $(i,i)$-th entry of $A^{-1}$ is $\text{Ring.inverse}(A_{i,i})$.

Matrix.add_mul_mul_inv_eq_sub theorem

 (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⁻¹

Full source

/-- The **Woodbury Identity** (`⁻¹` version). -/
theorem add_mul_mul_inv_eq_sub (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⁻¹ := by
  obtain ⟨_⟩ := hA.nonempty_invertible
  obtain ⟨_⟩ := hC.nonempty_invertible
  obtain ⟨iAC⟩ := hAC.nonempty_invertible
  simp only [← invOf_eq_nonsing_inv] at iAC
  letI := invertibleAddMulMul A U C V
  simp only [← invOf_eq_nonsing_inv]
  apply invOf_add_mul_mul

Woodbury Identity for Matrix Inversion: $(A + U C V)^{-1} = A^{-1} - A^{-1} U (C^{-1} + V A^{-1} U)^{-1} V A^{-1}$

Informal description

Let $A$, $C$ be square matrices over a ring $\alpha$ such that $A$ and $C$ are units (i.e., invertible), and let $U$, $V$ be matrices of appropriate dimensions. If $C^{-1} + V A^{-1} U$ is also a unit, then the inverse of $A + U C V$ exists and is given by: $$(A + U C V)^{-1} = A^{-1} - A^{-1} U (C^{-1} + V A^{-1} U)^{-1} V A^{-1}.$$

Matrix.inv_inv_inv theorem

(A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹

Full source

@[simp]
theorem inv_inv_inv (A : Matrix n n α) : A⁻¹A⁻¹⁻¹A⁻¹⁻¹⁻¹ = A⁻¹ := by
  by_cases h : IsUnit A.det
  · rw [nonsing_inv_nonsing_inv _ h]
  · simp [nonsing_inv_apply_not_isUnit _ h]

Triple Inverse Identity for Matrices: $(A^{-1})^{-1})^{-1} = A^{-1}$

Informal description

For any square matrix $A$ of size $n \times n$ over a ring $\alpha$, the triple inverse of $A$ equals the inverse of $A$, i.e., $(A^{-1})^{-1})^{-1} = A^{-1}$.

Matrix.inv_add_inv theorem

{A B : Matrix n n α} (h : IsUnit A ↔ IsUnit B) : A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹

Full source

/-- The `Matrix` version of `inv_add_inv'` -/
theorem inv_add_inv {A B : Matrix n n α} (h : IsUnitIsUnit A ↔ IsUnit B) :
    A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹ := by
  simpa only [nonsing_inv_eq_ringInverse] using Ring.inverse_add_inverse h

Sum of Inverses Formula for Matrices: $A^{-1} + B^{-1} = A^{-1}(A + B)B^{-1}$

Informal description

For any square matrices $A$ and $B$ of size $n \times n$ over a ring $\alpha$, if $A$ is invertible if and only if $B$ is invertible, then the sum of their inverses satisfies: $$A^{-1} + B^{-1} = A^{-1}(A + B)B^{-1}.$$

Matrix.inv_sub_inv theorem

{A B : Matrix n n α} (h : IsUnit A ↔ IsUnit B) : A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹

Full source

/-- The `Matrix` version of `inv_sub_inv'` -/
theorem inv_sub_inv {A B : Matrix n n α} (h : IsUnitIsUnit A ↔ IsUnit B) :
    A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹ := by
  simpa only [nonsing_inv_eq_ringInverse] using Ring.inverse_sub_inverse h

Difference of Inverses Formula: $A^{-1} - B^{-1} = A^{-1}(B - A)B^{-1}$

Informal description

For any square matrices $A$ and $B$ of size $n \times n$ over a ring $\alpha$, if $A$ is invertible if and only if $B$ is invertible, then the difference of their inverses satisfies $A^{-1} - B^{-1} = A^{-1} \cdot (B - A) \cdot B^{-1}$.

Matrix.mul_inv_rev theorem

(A B : Matrix n n α) : (A * B)⁻¹ = B⁻¹ * A⁻¹

Full source

theorem mul_inv_rev (A B : Matrix n n α) : (A * B)⁻¹ = B⁻¹ * A⁻¹ := by
  simp only [inv_def]
  rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]

Inverse of Matrix Product: $(AB)^{-1} = B^{-1}A^{-1}$

Informal description

For any invertible $n \times n$ matrices $A$ and $B$ over a ring $\alpha$, the inverse of their product equals the product of their inverses in reverse order: $$(AB)^{-1} = B^{-1}A^{-1}.$$

Matrix.list_prod_inv_reverse theorem

: ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.reverse.map Inv.inv).prod

Full source

/-- A version of `List.prod_inv_reverse` for `Matrix.inv`. -/
theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.reverse.map Inv.inv).prod
  | [] => by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
  | A::Xs => by
    rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,
      mul_inv_rev, list_prod_inv_reverse Xs]

Inverse of Matrix Product: $(\prod A_i)^{-1} = \prod A_i^{-1}$ in Reverse Order

Informal description

For any list $l$ of $n \times n$ matrices over a ring $\alpha$, the inverse of the product of matrices in $l$ equals the product of the inverses of the matrices in the reverse order of $l$. That is, $$ \left(\prod_{A \in l} A\right)^{-1} = \prod_{A \in \text{reverse}(l)} A^{-1}. $$

Matrix.det_smul_inv_mulVec_eq_cramer theorem

(A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹ *ᵥ b = cramer A b

Full source

/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/
@[simp]
theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :
    A.det • A⁻¹A⁻¹ *ᵥ b = cramer A b := by
  rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul,
    h.mul_val_inv, one_smul]

Cramer's Rule via Determinant and Inverse: $(\det A) \cdot (A^{-1} \cdot b) = \text{cramer}(A)(b)$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring $\alpha$ and any vector $b \in \alpha^n$, if the determinant $\det A$ is a unit in $\alpha$, then the scaled matrix-vector product of the inverse matrix $A^{-1}$ with $b$ equals the result of applying Cramer's rule to $A$ and $b$. That is, \[ (\det A) \cdot (A^{-1} \cdot b) = \text{cramer}(A)(b) \] where $\text{cramer}(A)(b)$ is the vector whose $i$-th component is the determinant of the matrix obtained by replacing the $i$-th column of $A$ with $b$.

Matrix.det_smul_inv_vecMul_eq_cramer_transpose theorem

(A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • b ᵥ* A⁻¹ = cramer Aᵀ b

Full source

/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/
@[simp]
theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :
    A.det • b ᵥ* A⁻¹ = cramer Aᵀ b := by
  rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]

Transposed Cramer's Rule via Determinant and Inverse: $(\det A) \cdot (b \cdot A^{-1}) = \text{cramer}(A^\top)(b)$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring $\alpha$ and any vector $b \in \alpha^n$, if the determinant $\det A$ is a unit in $\alpha$, then the scaled vector-matrix product of $b$ with the inverse matrix $A^{-1}$ equals the result of applying Cramer's rule to the transpose matrix $A^\top$ and $b$. That is, \[ (\det A) \cdot (b \cdot A^{-1}) = \text{cramer}(A^\top)(b) \] where $\text{cramer}(A^\top)(b)$ is the vector whose $i$-th component is the determinant of the matrix obtained by replacing the $i$-th column of $A^\top$ with $b$.

Matrix.submatrixEquivInvertible definition

(A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] : Invertible (A.submatrix e₁ e₂)

Full source

/-- `A.submatrix e₁ e₂` is invertible if `A` is -/
def submatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] :
    Invertible (A.submatrix e₁ e₂) :=
  invertibleOfRightInverse _ ((⅟ A).submatrix e₂ e₁) <| by
    rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]

Invertibility of submatrix via bijections

Informal description

Given a square matrix $A$ of size $m \times m$ over a type $\alpha$ with an invertible element structure, and given two bijections $e_1, e_2 : n \to m$, the submatrix $A.\text{submatrix}\, e_1\, e_2$ (obtained by selecting rows and columns according to $e_1$ and $e_2$) is invertible. The inverse of the submatrix is given by the corresponding submatrix of the inverse of $A$, specifically $(\text{⅟} A).\text{submatrix}\, e_2\, e_1$.

Matrix.invertibleOfSubmatrixEquivInvertible definition

(A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible (A.submatrix e₁ e₂)] : Invertible A

Full source

/-- `A` is invertible if `A.submatrix e₁ e₂` is -/
def invertibleOfSubmatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m)
    [Invertible (A.submatrix e₁ e₂)] : Invertible A :=
  invertibleOfRightInverse _ ((⅟ (A.submatrix e₁ e₂)).submatrix e₂.symm e₁.symm) <| by
    have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp
    conv in _ * _ =>
      congr
      rw [this]
    rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]

Invertibility of matrix via invertible submatrix

Informal description

Given a square matrix $A$ of size $m \times m$ over a type $\alpha$ and two bijections $e_1, e_2 : n \to m$, if the submatrix $A_{\text{submatrix}\, e_1\, e_2}$ (obtained by selecting rows and columns according to $e_1$ and $e_2$) is invertible, then the original matrix $A$ is also invertible. The inverse of $A$ can be constructed from the inverse of the submatrix.

Matrix.invOf_submatrix_equiv_eq theorem

 (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] [Invertible (A.submatrix e₁ e₂)] :
  ⅟ (A.submatrix e₁ e₂) = (⅟ A).submatrix e₂ e₁

Full source

theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A]
    [Invertible (A.submatrix e₁ e₂)] : ⅟ (A.submatrix e₁ e₂) = (⅟ A).submatrix e₂ e₁ := by
  rw [@Invertible.congr _ _ _ _ _ (submatrixEquivInvertible A e₁ e₂) rfl]
  rfl

Inverse of Permuted Submatrix Equals Permuted Inverse

Informal description

Let $A$ be an invertible $m \times m$ matrix over a type $\alpha$, and let $e_1, e_2 : n \to m$ be bijections. If the submatrix $A_{\text{submatrix}\, e_1\, e_2}$ is invertible, then the inverse of this submatrix is equal to the submatrix of the inverse of $A$ with rows and columns permuted according to $e_2$ and $e_1$, i.e., \[ \text{⅟}(A_{\text{submatrix}\, e_1\, e_2}) = (\text{⅟} A)_{\text{submatrix}\, e_2\, e_1}. \]

Matrix.submatrixEquivInvertibleEquivInvertible definition

(A : Matrix m m α) (e₁ e₂ : n ≃ m) : Invertible (A.submatrix e₁ e₂) ≃ Invertible A

Full source

/-- Together `Matrix.submatrixEquivInvertible` and
`Matrix.invertibleOfSubmatrixEquivInvertible` form an equivalence, although both sides of the
equiv are subsingleton anyway. -/
@[simps]
def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) :
    InvertibleInvertible (A.submatrix e₁ e₂) ≃ Invertible A where
  toFun _ := invertibleOfSubmatrixEquivInvertible A e₁ e₂
  invFun _ := submatrixEquivInvertible A e₁ e₂
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence between invertibility of matrix and its submatrix via bijections

Informal description

Given a square matrix $A$ of size $m \times m$ over a type $\alpha$ and two bijections $e_1, e_2 : n \to m$, there is an equivalence between the invertibility of the submatrix $A_{\text{submatrix}\, e_1\, e_2}$ (obtained by selecting rows and columns according to $e_1$ and $e_2$) and the invertibility of the original matrix $A$. This equivalence is constructed via the functions `invertibleOfSubmatrixEquivInvertible` and `submatrixEquivInvertible`, which respectively show that invertibility of the submatrix implies invertibility of $A$ and vice versa.

Matrix.isUnit_submatrix_equiv theorem

{A : Matrix m m α} (e₁ e₂ : n ≃ m) : IsUnit (A.submatrix e₁ e₂) ↔ IsUnit A

Full source

/-- When lowered to a prop, `Matrix.invertibleOfSubmatrixEquivInvertible` forms an `iff`. -/
@[simp]
theorem isUnit_submatrix_equiv {A : Matrix m m α} (e₁ e₂ : n ≃ m) :
    IsUnitIsUnit (A.submatrix e₁ e₂) ↔ IsUnit A := by
  simp only [← nonempty_invertible_iff_isUnit,
    (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]

Submatrix Unit Equivalence: $A_{\text{submatrix}\, e_1\, e_2}$ is a unit iff $A$ is a unit

Informal description

For any square matrix $A$ of size $m \times m$ over a type $\alpha$ and any bijections $e_1, e_2 : n \to m$, the submatrix $A_{\text{submatrix}\, e_1\, e_2}$ is a unit (i.e., has a multiplicative inverse) if and only if the original matrix $A$ is a unit.

Matrix.inv_submatrix_equiv theorem

(A : Matrix m m α) (e₁ e₂ : n ≃ m) : (A.submatrix e₁ e₂)⁻¹ = A⁻¹.submatrix e₂ e₁

Full source

@[simp]
theorem inv_submatrix_equiv (A : Matrix m m α) (e₁ e₂ : n ≃ m) :
    (A.submatrix e₁ e₂)⁻¹ = A⁻¹.submatrix e₂ e₁ := by
  by_cases h : IsUnit A
  · cases h.nonempty_invertible
    letI := submatrixEquivInvertible A e₁ e₂
    rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]
  · have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h
    simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this,
      submatrix_zero, Pi.zero_apply]

Inverse of Permuted Submatrix Equals Permuted Inverse: $(A_{\text{sub}\, e_1\, e_2})^{-1} = A^{-1}_{\text{sub}\, e_2\, e_1}$

Informal description

Let $A$ be an $m \times m$ matrix over a ring $\alpha$, and let $e_1, e_2 : n \to m$ be bijections. The inverse of the submatrix $A_{\text{submatrix}\, e_1\, e_2}$ is equal to the submatrix of $A^{-1}$ with rows and columns permuted according to $e_2$ and $e_1$, i.e., \[ (A_{\text{submatrix}\, e_1\, e_2})^{-1} = A^{-1}_{\text{submatrix}\, e_2\, e_1}. \]

Matrix.inv_reindex theorem

(e₁ e₂ : n ≃ m) (A : Matrix n n α) : (reindex e₁ e₂ A)⁻¹ = reindex e₂ e₁ A⁻¹

Full source

theorem inv_reindex (e₁ e₂ : n ≃ m) (A : Matrix n n α) : (reindex e₁ e₂ A)⁻¹ = reindex e₂ e₁ A⁻¹ :=
  inv_submatrix_equiv A e₁.symm e₂.symm

Inverse of Reindexed Matrix Equals Reindexed Inverse: $(\text{reindex}_{e_1, e_2} A)^{-1} = \text{reindex}_{e_2, e_1} A^{-1}$

Informal description

Let $A$ be an $n \times n$ matrix over a ring $\alpha$, and let $e_1, e_2 : n \to m$ be bijections. The inverse of the reindexed matrix $\text{reindex}_{e_1, e_2} A$ is equal to the reindexed inverse matrix $\text{reindex}_{e_2, e_1} A^{-1}$, i.e., \[ (\text{reindex}_{e_1, e_2} A)^{-1} = \text{reindex}_{e_2, e_1} A^{-1}. \]

Matrix.inv_kronecker theorem

[Fintype m] [DecidableEq m] (A : Matrix m m α) (B : Matrix n n α) : (A ⊗ₖ B)⁻¹ = A⁻¹ ⊗ₖ B⁻¹

Full source

theorem inv_kronecker [Fintype m] [DecidableEq m]
    (A : Matrix m m α) (B : Matrix n n α) : (A ⊗ₖ B)⁻¹ = A⁻¹A⁻¹ ⊗ₖ B⁻¹ := by
  -- handle the special cases where either matrix is not invertible
  by_cases hA : IsUnit A.det
  swap
  · cases isEmpty_or_nonempty n
    · subsingleton
    have hAB : ¬IsUnit (A ⊗ₖ B).det := by
      refine mt (fun hAB => ?_) hA
      rw [det_kronecker] at hAB
      exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
    rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]
  by_cases hB : IsUnit B.det; swap
  · cases isEmpty_or_nonempty m
    · subsingleton
    have hAB : ¬IsUnit (A ⊗ₖ B).det := by
      refine mt (fun hAB => ?_) hB
      rw [det_kronecker] at hAB
      exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)
    rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]
  -- otherwise follows trivially from `mul_kronecker_mul`
  · apply inv_eq_right_inv
    rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]

Inverse of Kronecker Product: $(A \otimes_k B)^{-1} = A^{-1} \otimes_k B^{-1}$

Informal description

Let $A$ be an $m \times m$ matrix and $B$ be an $n \times n$ matrix over a ring $\alpha$, where $m$ is finite and has decidable equality. Then the inverse of their Kronecker product equals the Kronecker product of their inverses, i.e., \[ (A \otimes_k B)^{-1} = A^{-1} \otimes_k B^{-1}. \]

Matrix.det_conj theorem

{M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : det (M * N * M⁻¹) = det N

Full source

/-- A variant of `Matrix.det_units_conj`. -/
theorem det_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
    det (M * N * M⁻¹) = det N := by rw [← h.unit_spec, ← coe_units_inv, det_units_conj]

Determinant Invariance under Conjugation by Invertible Matrix: $\det(M N M^{-1}) = \det(N)$

Informal description

For any square matrix $M$ of size $m \times m$ over a ring $\alpha$ that is a unit (i.e., invertible), and for any square matrix $N$ of the same size, the determinant of the conjugate $M N M^{-1}$ is equal to the determinant of $N$, i.e., \[ \det(M N M^{-1}) = \det(N). \]

Matrix.det_conj' theorem

{M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : det (M⁻¹ * N * M) = det N

Full source

/-- A variant of `Matrix.det_units_conj'`. -/
theorem det_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
    det (M⁻¹ * N * M) = det N := by rw [← h.unit_spec, ← coe_units_inv, det_units_conj']

Determinant Invariance under Conjugation by Invertible Matrix: $\det(M^{-1} N M) = \det(N)$

Informal description

For any square matrix $M$ of size $m \times m$ over a ring $\alpha$ that is invertible (i.e., $\text{IsUnit}\ M$ holds), and for any square matrix $N$ of the same size, the determinant of the conjugate $M^{-1} N M$ is equal to the determinant of $N$, i.e., \[ \det(M^{-1} N M) = \det(N). \]

Matrix.trace_conj theorem

{M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : trace (M * N * M⁻¹) = trace N

Full source

/-- A variant of `Matrix.trace_units_conj`. -/
theorem trace_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
    trace (M * N * M⁻¹) = trace N := by rw [← h.unit_spec, ← coe_units_inv, trace_units_conj]

Trace Invariance under Conjugation by Invertible Matrix: $\text{trace}(M N M^{-1}) = \text{trace}(N)$

Informal description

For any invertible square matrix $M$ of size $m \times m$ over a ring $\alpha$ and any square matrix $N$ of the same size, the trace of the conjugate $M N M^{-1}$ is equal to the trace of $N$, i.e., \[ \text{trace}(M N M^{-1}) = \text{trace}(N). \]

Matrix.trace_conj' theorem

{M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : trace (M⁻¹ * N * M) = trace N

Full source

/-- A variant of `Matrix.trace_units_conj'`. -/
theorem trace_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
    trace (M⁻¹ * N * M) = trace N := by rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']

Trace Invariance Under Conjugation: $\text{trace}(M^{-1} N M) = \text{trace}(N)$ for Invertible $M$

Informal description

For any square matrix $M$ of size $m \times m$ over a ring $\alpha$ that is a unit (i.e., invertible), and for any square matrix $N$ of the same size, the trace of $M^{-1} N M$ is equal to the trace of $N$.

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

References

Tags