Mathlib.LinearAlgebra.Matrix.Adjugate

Matrix.cramerMap definition

(i : n) : α

Full source

/-- `cramerMap A b i` is the determinant of the matrix `A` with column `i` replaced with `b`,
  and thus `cramerMap A b` is the vector output by Cramer's rule on `A` and `b`.

  If `A * x = b` has a unique solution in `x`, `cramerMap A` sends the vector `b` to `A.det • x`.
  Otherwise, the outcome of `cramerMap` is well-defined but not necessarily useful.
-/
def cramerMap (i : n) : α :=
  (A.updateCol i b).det

Cramer's rule vector component

Informal description

For a square matrix $ A $ of size $ n \times n $ over a commutative ring $ R $ and a vector $ b $, the function `cramerMap A b i` computes the determinant of the matrix obtained by replacing the $ i $-th column of $ A $ with $ b $. If the system $ A x = b $ has a unique solution $ x $, then `cramerMap A b` returns the vector $ (\det A) \cdot x $. Otherwise, the result is still well-defined but may not have a clear interpretation.

Matrix.cramerMap_is_linear theorem

(i : n) : IsLinearMap α fun b => cramerMap A b i

Full source

theorem cramerMap_is_linear (i : n) : IsLinearMap α fun b => cramerMap A b i :=
  { map_add := det_updateCol_add _ _
    map_smul := det_updateCol_smul _ _ }

Linearity of Cramer's Rule Component Function

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring $R$ and for any fixed column index $i$, the function $b \mapsto \text{cramerMap}(A, b, i)$ is a linear map from the vector space of column vectors $n \to R$ to $R$.

Matrix.cramer_is_linear theorem

: IsLinearMap α (cramerMap A)

Full source

theorem cramer_is_linear : IsLinearMap α (cramerMap A) := by
  constructor <;> intros <;> ext i
  · apply (cramerMap_is_linear A i).1
  · apply (cramerMap_is_linear A i).2

Linearity of Cramer's Rule Vector Function

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring $R$, the function $\text{cramerMap}(A, \cdot)$ is a linear map from the vector space of column vectors $n \to R$ to itself.

Matrix.cramer definition

(A : Matrix n n α) : (n → α) →ₗ[α] (n → α)

Full source

/-- `cramer A b i` is the determinant of the matrix `A` with column `i` replaced with `b`,
  and thus `cramer A b` is the vector output by Cramer's rule on `A` and `b`.

  If `A * x = b` has a unique solution in `x`, `cramer A` sends the vector `b` to `A.det • x`.
  Otherwise, the outcome of `cramer` is well-defined but not necessarily useful.
-/
def cramer (A : Matrix n n α) : (n → α) →ₗ[α] (n → α) :=
  IsLinearMap.mk' (cramerMap A) (cramer_is_linear A)

Cramer's rule linear map

Informal description

For a square matrix $ A $ of size $ n \times n $ over a commutative ring $ R $, the linear map $\text{cramer}(A)$ sends a vector $ b $ to the vector whose $ i $-th component is the determinant of the matrix obtained by replacing the $ i $-th column of $ A $ with $ b $. If the system $ A x = b $ has a unique solution $ x $, then $\text{cramer}(A)$ maps $ b $ to $ (\det A) \cdot x $. Otherwise, the result is still well-defined but may not have a meaningful interpretation.

Matrix.cramer_apply theorem

(i : n) : cramer A b i = (A.updateCol i b).det

Full source

theorem cramer_apply (i : n) : cramer A b i = (A.updateCol i b).det :=
  rfl

Componentwise Expression of Cramer's Rule: $\text{cramer}(A, b)_i = \det(A_{\text{updated}})$

Informal description

For a square matrix $A$ of size $n \times n$ over a commutative ring $R$, a vector $b \in R^n$, and an index $i \in n$, the $i$-th component of the vector obtained by applying Cramer's rule to $A$ and $b$ is equal to the determinant of the matrix formed by replacing the $i$-th column of $A$ with $b$. That is, \[ \text{cramer}(A, b)_i = \det(A_{\text{updated}}), \] where $A_{\text{updated}}$ is the matrix $A$ with its $i$-th column replaced by $b$.

Matrix.cramer_transpose_apply theorem

(i : n) : cramer Aᵀ b i = (A.updateRow i b).det

Full source

theorem cramer_transpose_apply (i : n) : cramer Aᵀ b i = (A.updateRow i b).det := by
  rw [cramer_apply, updateCol_transpose, det_transpose]

Cramer's Rule for Transpose Matrix: $\text{cramer}(A^\top, b)_i = \det(A_{\text{row }i \mapsto b})$

Informal description

For a square matrix $A$ of size $n \times n$ over a commutative ring $R$, a vector $b \in R^n$, and an index $i \in n$, the $i$-th component of the vector obtained by applying Cramer's rule to the transpose matrix $A^\top$ and $b$ is equal to the determinant of the matrix formed by replacing the $i$-th row of $A$ with $b$. That is, \[ \text{cramer}(A^\top, b)_i = \det(A_{\text{updated}}), \] where $A_{\text{updated}}$ is the matrix $A$ with its $i$-th row replaced by $b$.

Matrix.cramer_transpose_row_self theorem

(i : n) : Aᵀ.cramer (A i) = Pi.single i A.det

Full source

theorem cramer_transpose_row_self (i : n) : Aᵀ.cramer (A i) = Pi.single i A.det := by
  ext j
  rw [cramer_apply, Pi.single_apply]
  split_ifs with h
  · -- i = j: this entry should be `A.det`
    subst h
    simp only [updateCol_transpose, det_transpose, updateRow_eq_self]
  · -- i ≠ j: this entry should be 0
    rw [updateCol_transpose, det_transpose]
    apply det_zero_of_row_eq h
    rw [updateRow_self, updateRow_ne (Ne.symm h)]

Cramer's Rule Applied to Transpose Matrix Yields Determinant at Diagonal: $\text{cramer}(A^\top, A_i) = \text{single}_i(\det(A))$

Informal description

For a square matrix $A$ of size $n \times n$ over a commutative ring $R$ and an index $i \in n$, applying Cramer's rule to the transpose matrix $A^\top$ and the $i$-th row of $A$ yields the vector whose $i$-th component is $\det(A)$ and all other components are zero. That is, \[ \text{cramer}(A^\top, A_i) = \text{single}_i(\det(A)), \] where $\text{single}_i(\det(A))$ denotes the vector with $\det(A)$ at position $i$ and zero elsewhere.

Matrix.cramer_row_self theorem

(i : n) (h : ∀ j, b j = A j i) : A.cramer b = Pi.single i A.det

Full source

theorem cramer_row_self (i : n) (h : ∀ j, b j = A j i) : A.cramer b = Pi.single i A.det := by
  rw [← transpose_transpose A, det_transpose]
  convert cramer_transpose_row_self Aᵀ i
  exact funext h

Cramer's Rule for Matrix Column Yields Determinant at Diagonal: $\text{cramer}(A, A_{\cdot i}) = \text{single}_i(\det(A))$

Informal description

For a square matrix $A$ of size $n \times n$ over a commutative ring $R$, an index $i \in n$, and a vector $b$ such that $b_j = A_{j i}$ for all $j$, the vector obtained by applying Cramer's rule to $A$ and $b$ equals the vector whose $i$-th component is $\det(A)$ and all other components are zero. That is, \[ \text{cramer}(A, b) = \text{single}_i(\det(A)), \] where $\text{single}_i(\det(A))$ denotes the vector with $\det(A)$ at position $i$ and zero elsewhere.

Matrix.cramer_one theorem

: cramer (1 : Matrix n n α) = 1

Full source

@[simp]
theorem cramer_one : cramer (1 : Matrix n n α) = 1 := by
  ext i j
  convert congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j
  · simp
  · intro j
    rw [Matrix.one_eq_pi_single, Pi.single_comm]

Cramer's Rule for Identity Matrix: $\text{cramer}(1_n) = 1$

Informal description

The linear map $\text{cramer}(1_n)$ associated with the identity matrix $1_n$ of size $n \times n$ over a commutative ring $\alpha$ is equal to the identity linear map $1$ on $\alpha^n$.

Matrix.cramer_smul theorem

(r : α) (A : Matrix n n α) : cramer (r • A) = r ^ (Fintype.card n - 1) • cramer A

Full source

theorem cramer_smul (r : α) (A : Matrix n n α) :
    cramer (r • A) = r ^ (Fintype.card n - 1) • cramer A :=
  LinearMap.ext fun _ => funext fun _ => det_updateCol_smul_left _ _ _ _

Cramer's Rule Scaling Identity: $\text{cramer}(rA) = r^{n-1} \text{cramer}(A)$

Informal description

For any scalar $r$ in a commutative ring $R$ and any $n \times n$ matrix $A$ over $R$, the linear map $\text{cramer}(r \cdot A)$ is equal to $r^{n-1}$ times the linear map $\text{cramer}(A)$, where $n$ is the size of the matrix.

Matrix.cramer_subsingleton_apply theorem

[Subsingleton n] (A : Matrix n n α) (b : n → α) (i : n) : cramer A b i = b i

Full source

@[simp]
theorem cramer_subsingleton_apply [Subsingleton n] (A : Matrix n n α) (b : n → α) (i : n) :
    cramer A b i = b i := by rw [cramer_apply, det_eq_elem_of_subsingleton _ i, updateCol_self]

Cramer's Rule for Subsingleton Matrices: $\text{cramer}(A, b)_i = b_i$

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring $\alpha$, where the index type $n$ has at most one element (i.e., $n$ is a subsingleton type), and for any vector $b \in \alpha^n$ and index $i \in n$, the $i$-th component of the vector obtained by applying Cramer's rule to $A$ and $b$ is equal to the $i$-th component of $b$, i.e., \[ \text{cramer}(A, b)_i = b_i. \]

Matrix.cramer_zero theorem

[Nontrivial n] : cramer (0 : Matrix n n α) = 0

Full source

theorem cramer_zero [Nontrivial n] : cramer (0 : Matrix n n α) = 0 := by
  ext i j
  obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
  apply det_eq_zero_of_column_eq_zero j'
  intro j''
  simp [updateCol_ne hj']

Cramer's rule vanishes on the zero matrix

Informal description

For any nontrivial index type $n$ and any commutative ring $\alpha$, the Cramer's rule linear map associated with the zero matrix is the zero linear map, i.e., $\text{cramer}(0) = 0$.

Matrix.sum_cramer theorem

{β} (s : Finset β) (f : β → n → α) : (∑ x ∈ s, cramer A (f x)) = cramer A (∑ x ∈ s, f x)

Full source

/-- Use linearity of `cramer` to take it out of a summation. -/
theorem sum_cramer {β} (s : Finset β) (f : β → n → α) :
    (∑ x ∈ s, cramer A (f x)) = cramer A (∑ x ∈ s, f x) :=
  (map_sum (cramer A) ..).symm

Linearity of Cramer's Rule: Sum of Cramer Maps Equals Cramer Map of Sum

Informal description

For any finite set $s$ and any family of vectors $f \colon \beta \to n \to \alpha$ indexed by $s$, the sum of the Cramer's rule applications $\sum_{x \in s} \text{cramer}(A)(f(x))$ equals the Cramer's rule application of the sum of the vectors $\text{cramer}(A)\left(\sum_{x \in s} f(x)\right)$. Here, $\text{cramer}(A)$ is the linear map associated with a square matrix $A$ of size $n \times n$ over a commutative ring $\alpha$, which sends a vector $b$ to the vector whose $i$-th component is the determinant of the matrix obtained by replacing the $i$-th column of $A$ with $b$.

Matrix.sum_cramer_apply theorem

 {β} (s : Finset β) (f : n → β → α) (i : n) :
  (∑ x ∈ s, cramer A (fun j => f j x) i) = cramer A (fun j : n => ∑ x ∈ s, f j x) i

Full source

/-- Use linearity of `cramer` and vector evaluation to take `cramer A _ i` out of a summation. -/
theorem sum_cramer_apply {β} (s : Finset β) (f : n → β → α) (i : n) :
    (∑ x ∈ s, cramer A (fun j => f j x) i) = cramer A (fun j : n => ∑ x ∈ s, f j x) i :=
  calc
    (∑ x ∈ s, cramer A (fun j => f j x) i) = (∑ x ∈ s, cramer A fun j => f j x) i :=
      (Finset.sum_apply i s _).symm
    _ = cramer A (fun j : n => ∑ x ∈ s, f j x) i := by
      rw [sum_cramer, cramer_apply, cramer_apply]
      simp only [updateCol]
      congr with j
      congr
      apply Finset.sum_apply

Componentwise Linearity of Cramer's Rule: $\sum_{x \in s} \text{cramer}(A)(f_{\cdot}(x))_i = \text{cramer}(A)(\sum_{x \in s} f_{\cdot}(x))_i$

Informal description

For any finite set $s$ and any family of functions $f_j \colon \beta \to \alpha$ indexed by $j \in n$, the $i$-th component of the sum of Cramer's rule applications satisfies: \[ \sum_{x \in s} \text{cramer}(A)(f_{\cdot}(x))_i = \text{cramer}(A)\left(\sum_{x \in s} f_{\cdot}(x)\right)_i \] where $\text{cramer}(A)$ is the linear map associated with a square matrix $A$ of size $n \times n$ over a commutative ring $\alpha$, which sends a vector $b$ to the vector whose $i$-th component is the determinant of the matrix obtained by replacing the $i$-th column of $A$ with $b$.

Matrix.cramer_submatrix_equiv theorem

(A : Matrix m m α) (e : n ≃ m) (b : n → α) : cramer (A.submatrix e e) b = cramer A (b ∘ e.symm) ∘ e

Full source

theorem cramer_submatrix_equiv (A : Matrix m m α) (e : n ≃ m) (b : n → α) :
    cramer (A.submatrix e e) b = cramercramer A (b ∘ e.symm) ∘ e := by
  ext i
  simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,
    det_submatrix_equiv_self e, Function.comp_def]

Cramer's Rule Commutes with Submatrix via Index Bijection

Informal description

Let $A$ be an $m \times m$ matrix over a commutative ring $\alpha$, and let $e : n \simeq m$ be a bijection between the index sets $n$ and $m$. For any vector $b : n \to \alpha$, the application of Cramer's rule to the submatrix $A_{e(i),e(j)}$ and $b$ is equal to the composition of the application of Cramer's rule to $A$ and the vector $b \circ e^{-1}$, followed by $e$. In other words, the following equality holds: \[ \text{cramer}(A_{e(i),e(j)})(b) = \text{cramer}(A)(b \circ e^{-1}) \circ e. \]

Matrix.cramer_reindex theorem

(e : m ≃ n) (A : Matrix m m α) (b : n → α) : cramer (reindex e e A) b = cramer A (b ∘ e) ∘ e.symm

Full source

theorem cramer_reindex (e : m ≃ n) (A : Matrix m m α) (b : n → α) :
    cramer (reindex e e A) b = cramercramer A (b ∘ e) ∘ e.symm :=
  cramer_submatrix_equiv _ _ _

Cramer's Rule Commutes with Matrix Reindexing via Bijection $e$

Informal description

Let $A$ be an $m \times m$ matrix over a commutative ring $\alpha$, and let $e : m \simeq n$ be a bijection between the index sets $m$ and $n$. For any vector $b : n \to \alpha$, the application of Cramer's rule to the reindexed matrix $A_{e^{-1}(i),e^{-1}(j)}$ and $b$ is equal to the composition of the application of Cramer's rule to $A$ and the vector $b \circ e$, followed by $e^{-1}$. In other words, the following equality holds: \[ \text{cramer}(A_{e^{-1}(i),e^{-1}(j)})(b) = \text{cramer}(A)(b \circ e) \circ e^{-1}. \]

Matrix.adjugate definition

(A : Matrix n n α) : Matrix n n α

Full source

/-- The adjugate matrix is the transpose of the cofactor matrix.

  Typically, the cofactor matrix is defined by taking minors,
  i.e. the determinant of the matrix with a row and column removed.
  However, the proof of `mul_adjugate` becomes a lot easier if we use the
  matrix replacing a column with a basis vector, since it allows us to use
  facts about the `cramer` map.
-/
def adjugate (A : Matrix n n α) : Matrix n n α :=
  of fun i => cramer Aᵀ (Pi.single i 1)

Adjugate matrix

Informal description

The adjugate matrix of a square matrix $ A $ of size $ n \times n $ over a commutative ring is the transpose of the cofactor matrix. For each index $ i $, the $ i $-th column of the adjugate matrix is given by applying Cramer's rule to the transpose of $ A $ and the $ i $-th standard basis vector $ \mathbf{e}_i $. Explicitly, the entry at position $ (i, j) $ in the adjugate matrix is the determinant of the matrix obtained by replacing the $ j $-th row of $ A $ with the $ i $-th standard basis vector.

Matrix.adjugate_def theorem

(A : Matrix n n α) : adjugate A = of fun i => cramer Aᵀ (Pi.single i 1)

Full source

theorem adjugate_def (A : Matrix n n α) : adjugate A = of fun i => cramer Aᵀ (Pi.single i 1) :=
  rfl

Definition of Adjugate Matrix via Cramer's Rule

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring, the adjugate matrix $\text{adjugate}(A)$ is defined as the matrix whose $i$-th column is given by applying Cramer's rule to the transpose matrix $A^T$ and the $i$-th standard basis vector $\mathbf{e}_i$ (represented as $\text{Pi.single } i 1$). Explicitly, $\text{adjugate}(A) = \text{of } (\lambda i, \text{cramer}(A^T)(\mathbf{e}_i))$, where $\text{of}$ constructs a matrix from a column-generating function.

Matrix.adjugate_apply theorem

(A : Matrix n n α) (i j : n) : adjugate A i j = (A.updateRow j (Pi.single i 1)).det

Full source

theorem adjugate_apply (A : Matrix n n α) (i j : n) :
    adjugate A i j = (A.updateRow j (Pi.single i 1)).det := by
  rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_transpose]

Entrywise Formula for Adjugate Matrix: $(\text{adjugate}(A))_{i,j} = \det(A_{\text{updated}})$

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring, the $(i,j)$-th entry of the adjugate matrix $\text{adjugate}(A)$ is equal to the determinant of the matrix obtained by replacing the $j$-th row of $A$ with the $i$-th standard basis vector $\mathbf{e}_i$ (represented as $\text{Pi.single } i 1$). In symbols: \[ (\text{adjugate}(A))_{i,j} = \det(A_{\text{updated}}), \] where $A_{\text{updated}}$ is the matrix $A$ with its $j$-th row replaced by $\mathbf{e}_i$.

Matrix.adjugate_transpose theorem

(A : Matrix n n α) : (adjugate A)ᵀ = adjugate Aᵀ

Full source

theorem adjugate_transpose (A : Matrix n n α) : (adjugate A)ᵀ = adjugate Aᵀ := by
  ext i j
  rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_transpose]
  rw [det_apply', det_apply']
  apply Finset.sum_congr rfl
  intro σ _
  congr 1
  by_cases h : i = σ j
  · -- Everything except `(i , j)` (= `(σ j , j)`) is given by A, and the rest is a single `1`.
    congr
    ext j'
    subst h
    have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff
    rw [updateRow_apply, updateCol_apply]
    simp_rw [this]
    rw [← dite_eq_ite, ← dite_eq_ite]
    congr 1 with rfl
    rw [Pi.single_eq_same, Pi.single_eq_same]
  · -- Otherwise, we need to show that there is a `0` somewhere in the product.
    have : (∏ j' : n, updateCol A j (Pi.single i 1) (σ j') j') = 0 := by
      apply prod_eq_zero (mem_univ j)
      rw [updateCol_self, Pi.single_eq_of_ne' h]
    rw [this]
    apply prod_eq_zero (mem_univ (σ⁻¹ i))
    erw [apply_symm_apply σ i, updateRow_self]
    apply Pi.single_eq_of_ne
    intro h'
    exact h ((symm_apply_eq σ).mp h')

Transpose-Adjugate Commutation: $(\text{adjugate}(A))^\top = \text{adjugate}(A^\top)$

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring, the transpose of the adjugate matrix of $A$ is equal to the adjugate matrix of the transpose of $A$, i.e., \[ (\text{adjugate}(A))^\top = \text{adjugate}(A^\top). \]

Matrix.adjugate_submatrix_equiv_self theorem

(e : n ≃ m) (A : Matrix m m α) : adjugate (A.submatrix e e) = (adjugate A).submatrix e e

Full source

@[simp]
theorem adjugate_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m α) :
    adjugate (A.submatrix e e) = (adjugate A).submatrix e e := by
  ext i j
  have : (fun j ↦ Pi.single i 1 <| e.symm j) = Pi.single (e i) 1 :=
    Function.update_comp_equiv (0 : n → α) e.symm i 1
  rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]

Adjugate Commutes with Submatrix via Bijection: $\text{adjugate}(A_{e(i),e(j)}) = (\text{adjugate}\, A)_{e(i),e(j)}$

Informal description

Let $A$ be an $m \times m$ matrix over a commutative ring, and let $e : n \simeq m$ be a bijection between the index sets $n$ and $m$. Then the adjugate of the submatrix $A_{e(i),e(j)}$ is equal to the submatrix of the adjugate of $A$ obtained by applying the same bijection $e$ to both rows and columns. In symbols: \[ \text{adjugate}(A_{e(i),e(j)}) = (\text{adjugate}\, A)_{e(i),e(j)}. \]

Matrix.adjugate_reindex theorem

(e : m ≃ n) (A : Matrix m m α) : adjugate (reindex e e A) = reindex e e (adjugate A)

Full source

theorem adjugate_reindex (e : m ≃ n) (A : Matrix m m α) :
    adjugate (reindex e e A) = reindex e e (adjugate A) :=
  adjugate_submatrix_equiv_self _ _

Adjugate Commutes with Reindexing: $\text{adjugate}(A_{e(i),e(j)}) = (\text{adjugate}\, A)_{e(i),e(j)}$

Informal description

Let $A$ be an $m \times m$ matrix over a commutative ring, and let $e : m \simeq n$ be a bijection between the index sets $m$ and $n$. Then the adjugate of the reindexed matrix $A_{e(i),e(j)}$ is equal to the reindexing of the adjugate of $A$ via the same bijection $e$. In symbols: \[ \text{adjugate}(A_{e(i),e(j)}) = (\text{adjugate}\, A)_{e(i),e(j)}. \]

Matrix.cramer_eq_adjugate_mulVec theorem

(A : Matrix n n α) (b : n → α) : cramer A b = A.adjugate *ᵥ b

Full source

/-- Since the map `b ↦ cramer A b` is linear in `b`, it must be multiplication by some matrix. This
matrix is `A.adjugate`. -/
theorem cramer_eq_adjugate_mulVec (A : Matrix n n α) (b : n → α) :
    cramer A b = A.adjugate *ᵥ b := by
  nth_rw 2 [← A.transpose_transpose]
  rw [← adjugate_transpose, adjugate_def]
  have : b = ∑ i, b i • (Pi.single i 1 : n → α) := by
    refine (pi_eq_sum_univ b).trans ?_
    congr with j
    simp [Pi.single_apply, eq_comm]
  conv_lhs =>
    rw [this]
  ext k
  simp [mulVec, dotProduct, mul_comm]

Cramer's Rule as Adjugate-Vector Product: $\text{cramer}(A)(b) = (\text{adjugate}\, A) \cdot b$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring and any vector $b \in \alpha^n$, the result of applying Cramer's rule to $A$ and $b$ is equal to the matrix-vector product of the adjugate matrix of $A$ with $b$. That is, \[ \text{cramer}(A)(b) = (\text{adjugate}\, A) \cdot 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.mul_adjugate_apply theorem

(A : Matrix n n α) (i j k) : A i k * adjugate A k j = cramer Aᵀ (Pi.single k (A i k)) j

Full source

theorem mul_adjugate_apply (A : Matrix n n α) (i j k) :
    A i k * adjugate A k j = cramer Aᵀ (Pi.single k (A i k)) j := by
  rw [← smul_eq_mul, adjugate, of_apply, ← Pi.smul_apply, ← LinearMap.map_smul, ← Pi.single_smul',
    smul_eq_mul, mul_one]

Entry-wise Product with Adjugate Equals Cramer's Rule on Transpose

Informal description

For any $n \times n$ matrix $A$ over a commutative ring and any indices $i, j, k$, the entry-wise product of $A_{i,k}$ with the $(k,j)$-th entry of the adjugate matrix of $A$ equals the $j$-th component of the vector obtained by applying Cramer's rule to the transpose matrix $A^\top$ and the vector $\mathbf{e}_k \cdot A_{i,k}$, where $\mathbf{e}_k$ is the $k$-th standard basis vector. In symbols: $$ A_{i,k} \cdot (\text{adjugate } A)_{k,j} = \text{cramer}(A^\top)(A_{i,k} \cdot \mathbf{e}_k)_j $$

Matrix.mul_adjugate theorem

(A : Matrix n n α) : A * adjugate A = A.det • (1 : Matrix n n α)

Full source

theorem mul_adjugate (A : Matrix n n α) : A * adjugate A = A.det • (1 : Matrix n n α) := by
  ext i j
  rw [mul_apply, Pi.smul_apply, Pi.smul_apply, one_apply, smul_eq_mul, mul_boole]
  simp [mul_adjugate_apply, sum_cramer_apply, cramer_transpose_row_self, Pi.single_apply, eq_comm]

Matrix Product with Adjugate Equals Determinant Times Identity: $A \cdot \text{adjugate}(A) = (\det A) I_n$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring, the product of $A$ with its adjugate matrix equals the determinant of $A$ times the identity matrix. That is, $$ A \cdot \text{adjugate}(A) = (\det A) \cdot I_n $$ where $I_n$ is the $n \times n$ identity matrix.

Matrix.adjugate_mul theorem

(A : Matrix n n α) : adjugate A * A = A.det • (1 : Matrix n n α)

Full source

theorem adjugate_mul (A : Matrix n n α) : adjugate A * A = A.det • (1 : Matrix n n α) :=
  calc
    adjugate A * A = (Aᵀ * adjugate Aᵀ)ᵀ := by
      rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]
    _ = _ := by rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]

Adjugate-Matrix Product Equals Determinant Times Identity: $\text{adjugate}(A) \cdot A = (\det A) I_n$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring, the product of the adjugate matrix of $A$ with $A$ equals the determinant of $A$ times the identity matrix. That is, $$ \text{adjugate}(A) \cdot A = (\det A) \cdot I_n $$ where $I_n$ is the $n \times n$ identity matrix.

Matrix.adjugate_smul theorem

(r : α) (A : Matrix n n α) : adjugate (r • A) = r ^ (Fintype.card n - 1) • adjugate A

Full source

theorem adjugate_smul (r : α) (A : Matrix n n α) :
    adjugate (r • A) = r ^ (Fintype.card n - 1) • adjugate A := by
  rw [adjugate, adjugate, transpose_smul, cramer_smul]
  rfl

Adjugate Scaling Identity: $\text{adjugate}(rA) = r^{n-1} \text{adjugate}(A)$

Informal description

For any scalar $r$ in a commutative ring $R$ and any $n \times n$ matrix $A$ over $R$, the adjugate of the scaled matrix $rA$ is equal to $r^{n-1}$ times the adjugate of $A$, where $n$ is the size of the matrix.

Matrix.mulVec_cramer theorem

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

Full source

/-- A stronger form of **Cramer's rule** that allows us to solve some instances of `A * x = b` even
if the determinant is not a unit. A sufficient (but still not necessary) condition is that `A.det`
divides `b`. -/
@[simp]
theorem mulVec_cramer (A : Matrix n n α) (b : n → α) : A *ᵥ cramer A b = A.det • b := by
  rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec_assoc, one_mulVec]

Matrix-Vector Product via Cramer's Rule: $A \cdot \text{cramer}(A)(b) = (\det A) b$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring and any vector $b \in \alpha^n$, the matrix-vector product of $A$ with the result of applying Cramer's rule to $A$ and $b$ equals the determinant of $A$ times $b$. That is, $$ A \cdot \text{cramer}(A)(b) = (\det A) \cdot 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.adjugate_subsingleton theorem

[Subsingleton n] (A : Matrix n n α) : adjugate A = 1

Full source

theorem adjugate_subsingleton [Subsingleton n] (A : Matrix n n α) : adjugate A = 1 := by
  ext i j
  simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i, one_apply]

Adjugate of Subsingleton Matrix is Identity

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring $\alpha$, where the index type $n$ has at most one element (i.e., $n$ is a subsingleton type), the adjugate of $A$ is equal to the identity matrix $1$.

Matrix.adjugate_eq_one_of_card_eq_one theorem

{A : Matrix n n α} (h : Fintype.card n = 1) : adjugate A = 1

Full source

theorem adjugate_eq_one_of_card_eq_one {A : Matrix n n α} (h : Fintype.card n = 1) :
    adjugate A = 1 :=
  haveI : Subsingleton n := Fintype.card_le_one_iff_subsingleton.mp h.le
  adjugate_subsingleton _

Adjugate Matrix is Identity for 1×1 Matrices

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring $\alpha$, if the index set $n$ has cardinality 1 (i.e., $|n| = 1$), then the adjugate matrix of $A$ equals the identity matrix, i.e., $\text{adjugate}(A) = 1$.

Matrix.adjugate_zero theorem

[Nontrivial n] : adjugate (0 : Matrix n n α) = 0

Full source

@[simp]
theorem adjugate_zero [Nontrivial n] : adjugate (0 : Matrix n n α) = 0 := by
  ext i j
  obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
  apply det_eq_zero_of_column_eq_zero j'
  intro j''
  simp [updateCol_ne hj']

Adjugate of Zero Matrix is Zero

Informal description

For any nontrivial index type $n$ and any commutative ring $\alpha$, the adjugate of the zero matrix of size $n \times n$ is the zero matrix, i.e., $\text{adjugate}(0) = 0$.

Matrix.adjugate_one theorem

: adjugate (1 : Matrix n n α) = 1

Full source

@[simp]
theorem adjugate_one : adjugate (1 : Matrix n n α) = 1 := by
  ext
  simp [adjugate_def, Matrix.one_apply, Pi.single_apply, eq_comm]

Adjugate of Identity Matrix is Identity

Informal description

The adjugate of the identity matrix of size $n \times n$ over a commutative ring $\alpha$ is the identity matrix, i.e., $\text{adjugate}(1_n) = 1_n$.

Matrix.adjugate_diagonal theorem

(v : n → α) : adjugate (diagonal v) = diagonal fun i => ∏ j ∈ Finset.univ.erase i, v j

Full source

@[simp]
theorem adjugate_diagonal (v : n → α) :
    adjugate (diagonal v) = diagonal fun i => ∏ j ∈ Finset.univ.erase i, v j := by
  ext i j
  simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]
  obtain rfl | hij := eq_or_ne i j
  · rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
  · rw [diagonal_apply_ne _ hij]
    refine det_eq_zero_of_row_eq_zero j fun k => ?_
    obtain rfl | hjk := eq_or_ne k j
    · rw [updateCol_self, Pi.single_eq_of_ne' hij]
    · rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]

Adjugate of Diagonal Matrix is Diagonal with Product of Off-Diagonal Entries

Informal description

For any vector $v : n \to \alpha$ defining a diagonal matrix, the adjugate of the diagonal matrix $\text{diagonal } v$ is also a diagonal matrix. Specifically, the $(i,i)$-th entry of the adjugate matrix is the product of all entries $v_j$ for $j \neq i$, i.e., \[ \text{adjugate}(\text{diagonal } v) = \text{diagonal } \left( \lambda i, \prod_{j \neq i} v_j \right). \]

RingHom.map_adjugate theorem

 {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) (M : Matrix n n R) :
  f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M)

Full source

theorem _root_.RingHom.map_adjugate {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
    (M : Matrix n n R) : f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M) := by
  ext i k
  have : Pi.single i (1 : S) = f ∘ Pi.single i 1 := by
    rw [← f.map_one]
    exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)
  rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]

Adjugate Matrix Preservation under Ring Homomorphism: $f(\text{adjugate}(M)) = \text{adjugate}(f(M))$

Informal description

For any commutative rings $R$ and $S$, and any ring homomorphism $f \colon R \to S$, the adjugate of a matrix $M$ over $R$ is preserved under $f$. That is, applying $f$ entry-wise to the adjugate of $M$ yields the adjugate of the matrix obtained by applying $f$ entry-wise to $M$: \[ f(\text{adjugate}(M)) = \text{adjugate}(f(M)). \]

AlgHom.map_adjugate theorem

 {R A B : Type*} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B)
  (M : Matrix n n A) : f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M)

Full source

theorem _root_.AlgHom.map_adjugate {R A B : Type*} [CommSemiring R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (M : Matrix n n A) :
    f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M) :=
  f.toRingHom.map_adjugate _

Adjugate Matrix Preservation under Algebra Homomorphism: $f(\text{adjugate}(M)) = \text{adjugate}(f(M))$

Informal description

Let $R$ be a commutative semiring and $A$, $B$ be commutative rings with $R$-algebra structures. For any $R$-algebra homomorphism $f \colon A \to B$ and any square matrix $M$ of size $n \times n$ over $A$, the adjugate matrix is preserved under $f$, i.e., \[ f(\text{adjugate}(M)) = \text{adjugate}(f(M)), \] where $f$ is applied entry-wise to the matrices.

Matrix.det_adjugate theorem

(A : Matrix n n α) : (adjugate A).det = A.det ^ (Fintype.card n - 1)

Full source

theorem det_adjugate (A : Matrix n n α) : (adjugate A).det = A.det ^ (Fintype.card n - 1) := by
  -- get rid of the `- 1`
  rcases (Fintype.card n).eq_zero_or_pos with h_card | h_card
  · haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card
    rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_one]
  replace h_card := tsub_add_cancel_of_le h_card.nat_succ_le
  -- express `A` as an evaluation of a polynomial in n^2 variables, and solve in the polynomial ring
  -- where `A'.det` is non-zero.
  let A' := mvPolynomialX n n ℤ
  suffices A'.adjugate.det = A'.det ^ (Fintype.card n - 1) by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, this]
  apply mul_left_cancel₀ (show A'.det ≠ 0 from det_mvPolynomialX_ne_zero n ℤ)
  calc
    A'.det * A'.adjugate.det = (A' * adjugate A').det := (det_mul _ _).symm
    _ = A'.det ^ Fintype.card n := by rw [mul_adjugate, det_smul, det_one, mul_one]
    _ = A'.det * A'.det ^ (Fintype.card n - 1) := by rw [← pow_succ', h_card]

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

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring, the determinant of its adjugate matrix equals the determinant of $A$ raised to the power of $n-1$, i.e., \[ \det(\text{adjugate}(A)) = (\det A)^{n-1}. \]

Matrix.adjugate_fin_zero theorem

(A : Matrix (Fin 0) (Fin 0) α) : adjugate A = 0

Full source

@[simp]
theorem adjugate_fin_zero (A : Matrix (Fin 0) (Fin 0) α) : adjugate A = 0 :=
  Subsingleton.elim _ _

Adjugate of Zero-Sized Matrix is Zero

Informal description

For any square matrix $A$ of size $0 \times 0$ over a commutative ring, the adjugate matrix of $A$ is the zero matrix.

Matrix.adjugate_fin_one theorem

(A : Matrix (Fin 1) (Fin 1) α) : adjugate A = 1

Full source

@[simp]
theorem adjugate_fin_one (A : Matrix (Fin 1) (Fin 1) α) : adjugate A = 1 :=
  adjugate_subsingleton A

Adjugate of $1 \times 1$ Matrix is Identity

Informal description

For any $1 \times 1$ matrix $A$ over a commutative ring, the adjugate of $A$ is the identity matrix $1$.

Matrix.adjugate_fin_succ_eq_det_submatrix theorem

 {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) α) (i j) :
  adjugate A i j = (-1) ^ (j + i : ℕ) * det (A.submatrix j.succAbove i.succAbove)

Full source

theorem adjugate_fin_succ_eq_det_submatrix {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) α) (i j) :
    adjugate A i j = (-1) ^ (j + i : ℕ) * det (A.submatrix j.succAbove i.succAbove) := by
  simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]
  rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]
  rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]

Adjugate Matrix Entry Formula via Cofactors: $(\text{adjugate}(A))_{i,j} = (-1)^{i+j} \det(A_{j^c,i^c})$

Informal description

For any $(n+1) \times (n+1)$ matrix $A$ over a commutative ring and any indices $i,j \in \{0,\dots,n\}$, the $(i,j)$-th entry of the adjugate matrix $\text{adjugate}(A)$ is given by: \[ (\text{adjugate}(A))_{i,j} = (-1)^{i+j} \cdot \det(A_{j^c,i^c}) \] where $A_{j^c,i^c}$ denotes the submatrix obtained by removing the $j$-th row and $i$-th column from $A$.

Matrix.adjugate_fin_two theorem

(A : Matrix (Fin 2) (Fin 2) α) : adjugate A = !![A 1 1, -A 0 1; -A 1 0, A 0 0]

Full source

theorem adjugate_fin_two (A : Matrix (Fin 2) (Fin 2) α) :
    adjugate A = !![A 1 1, -A 0 1; -A 1 0, A 0 0] := by
  ext i j
  rw [adjugate_fin_succ_eq_det_submatrix]
  fin_cases i <;> fin_cases j <;> simp

Adjugate Formula for $2 \times 2$ Matrices: $\text{adjugate}\begin{pmatrix} a & b \\ c & d \end{pmatrix} = \begin{pmatrix} d & -b \\ -c & a \end{pmatrix}$

Informal description

For any $2 \times 2$ matrix $A = \begin{pmatrix} a & b \\ c & d \end{pmatrix}$ over a commutative ring, the adjugate matrix is given by: \[ \text{adjugate}(A) = \begin{pmatrix} d & -b \\ -c & a \end{pmatrix}. \]

Matrix.adjugate_fin_two_of theorem

(a b c d : α) : adjugate !![a, b; c, d] = !![d, -b; -c, a]

Full source

@[simp]
theorem adjugate_fin_two_of (a b c d : α) : adjugate !![a, b; c, d] = !![d, -b; -c, a] :=
  adjugate_fin_two _

Adjugate Formula for $2 \times 2$ Matrices: $\text{adjugate}\begin{pmatrix} a & b \\ c & d \end{pmatrix} = \begin{pmatrix} d & -b \\ -c & a \end{pmatrix}$

Informal description

For any elements $a, b, c, d$ in a commutative ring $\alpha$, the adjugate of the $2 \times 2$ matrix $\begin{pmatrix} a & b \\ c & d \end{pmatrix}$ is given by: \[ \text{adjugate}\begin{pmatrix} a & b \\ c & d \end{pmatrix} = \begin{pmatrix} d & -b \\ -c & a \end{pmatrix}. \]

Matrix.adjugate_fin_three theorem

 (A : Matrix (Fin 3) (Fin 3) α) :
  adjugate A =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
      -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
      A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]

Full source

theorem adjugate_fin_three (A : Matrix (Fin 3) (Fin 3) α) :
    adjugate A =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1,
      -(A 0 1 * A 2 2) + A 0 2 * A 2 1,
      A 0 1 * A 1 2 - A 0 2 * A 1 1;
      -(A 1 0 * A 2 2) + A 1 2 * A 2 0,
      A 0 0 * A 2 2 - A 0 2 * A 2 0,
      -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
      A 1 0 * A 2 1 - A 1 1 * A 2 0,
      -(A 0 0 * A 2 1) + A 0 1 * A 2 0,
      A 0 0 * A 1 1 - A 0 1 * A 1 0] := by
  ext i j
  rw [adjugate_fin_succ_eq_det_submatrix, det_fin_two]
  fin_cases i <;> fin_cases j <;> simp [updateRow, Fin.succAbove, Fin.lt_def] <;> ring

Adjugate Matrix Formula for $3 \times 3$ Matrices

Informal description

For any $3 \times 3$ matrix $A$ over a commutative ring $\alpha$, the adjugate matrix $\text{adjugate}(A)$ is given by: \[ \text{adjugate}(A) = \begin{bmatrix} A_{11}A_{22} - A_{12}A_{21} & -(A_{01}A_{22}) + A_{02}A_{21} & A_{01}A_{12} - A_{02}A_{11} \\ -(A_{10}A_{22}) + A_{12}A_{20} & A_{00}A_{22} - A_{02}A_{20} & -(A_{00}A_{12}) + A_{02}A_{10} \\ A_{10}A_{21} - A_{11}A_{20} & -(A_{00}A_{21}) + A_{01}A_{20} & A_{00}A_{11} - A_{01}A_{10} \end{bmatrix} \] where $A_{ij}$ denotes the entry in the $i$-th row and $j$-th column of $A$.

Matrix.adjugate_fin_three_of theorem

 (a b c d e f g h i : α) :
  adjugate !![a, b, c; d, e, f; g, h, i] =
    !![e * i - f * h, -(b * i) + c * h, b * f - c * e;
      -(d * i) + f * g, a * i - c * g, -(a * f) + c * d;
      d * h - e * g, -(a * h) + b * g, a * e - b * d]

Full source

@[simp]
theorem adjugate_fin_three_of (a b c d e f g h i : α) :
    adjugate !![a, b, c; d, e, f; g, h, i] =
      !![  e * i  - f * h, -(b * i) + c * h,   b * f  - c * e;
         -(d * i) + f * g,   a * i  - c * g, -(a * f) + c * d;
           d * h  - e * g, -(a * h) + b * g,   a * e  - b * d] :=
  adjugate_fin_three _

Adjugate Matrix Formula for $3 \times 3$ Matrices with Explicit Entries

Informal description

For any $3 \times 3$ matrix over a commutative ring $\alpha$ with entries $a, b, c, d, e, f, g, h, i$, the adjugate matrix is given by: \[ \text{adjugate}\begin{pmatrix} a & b & c \\ d & e & f \\ g & h & i \end{pmatrix} = \begin{pmatrix} ei - fh & -(bi) + ch & bf - ce \\ -(di) + fg & ai - cg & -(af) + cd \\ dh - eg & -(ah) + bg & ae - bd \end{pmatrix} \]

Matrix.det_eq_sum_mul_adjugate_row theorem

(A : Matrix n n α) (i : n) : det A = ∑ j : n, A i j * adjugate A j i

Full source

theorem det_eq_sum_mul_adjugate_row (A : Matrix n n α) (i : n) :
    det A = ∑ j : n, A i j * adjugate A j i := by
  haveI : Nonempty n := ⟨i⟩
  obtain ⟨n', hn'⟩ := Nat.exists_eq_succ_of_ne_zero (Fintype.card_ne_zero : Fintype.cardFintype.card n ≠ 0)
  obtain ⟨e⟩ := Fintype.truncEquivFinOfCardEq hn'
  let A' := reindex e e A
  suffices det A' = ∑ j : Fin n'.succ, A' (e i) j * adjugate A' j (e i) by
    simp_rw [A', det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,
      Equiv.symm_apply_apply] at this
    exact this
  rw [det_succ_row A' (e i)]
  simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]

Laplace Expansion via Adjugate: $\det(A) = \sum_j A_{ij} (\text{adjugate}\, A)_{ji}$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring $\alpha$ and any row index $i$, the determinant of $A$ can be expressed as the dot product of the $i$-th row of $A$ with the $i$-th column of the adjugate matrix of $A$. That is: \[ \det(A) = \sum_{j=1}^n A_{ij} \cdot (\text{adjugate}\, A)_{ji} \]

Matrix.det_eq_sum_mul_adjugate_col theorem

(A : Matrix n n α) (j : n) : det A = ∑ i : n, A i j * adjugate A j i

Full source

theorem det_eq_sum_mul_adjugate_col (A : Matrix n n α) (j : n) :
    det A = ∑ i : n, A i j * adjugate A j i := by
  simpa only [det_transpose, ← adjugate_transpose] using det_eq_sum_mul_adjugate_row Aᵀ j

Laplace Expansion via Adjugate: $\det(A) = \sum_i A_{ij} (\text{adjugate}\, A)_{ji}$ (column version)

Informal description

For any $n \times n$ matrix $A$ over a commutative ring $\alpha$ and any column index $j$, the determinant of $A$ can be expressed as the dot product of the $j$-th column of $A$ with the $j$-th row of the adjugate matrix of $A$. That is: \[ \det(A) = \sum_{i=1}^n A_{ij} \cdot (\text{adjugate}\, A)_{ji} \]

Matrix.adjugate_conjTranspose theorem

[StarRing α] (A : Matrix n n α) : A.adjugateᴴ = adjugate Aᴴ

Full source

theorem adjugate_conjTranspose [StarRing α] (A : Matrix n n α) : A.adjugateᴴ = adjugate Aᴴ := by
  dsimp only [conjTranspose]
  have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ
  rw [A.adjugate_transpose, this]

Conjugate Transpose-Adjugate Commutation: $(\text{adjugate}(A))^\dagger = \text{adjugate}(A^\dagger)$

Informal description

For any square matrix $A$ of size $n \times n$ over a commutative ring $\alpha$ equipped with a star ring structure, the conjugate transpose of the adjugate matrix of $A$ is equal to the adjugate matrix of the conjugate transpose of $A$, i.e., \[ (\text{adjugate}(A))^\dagger = \text{adjugate}(A^\dagger). \]

Matrix.isRegular_of_isLeftRegular_det theorem

{A : Matrix n n α} (hA : IsLeftRegular A.det) : IsRegular A

Full source

theorem isRegular_of_isLeftRegular_det {A : Matrix n n α} (hA : IsLeftRegular A.det) :
    IsRegular A := by
  constructor
  · intro B C h
    refine hA.matrix ?_
    simp only at h ⊢
    rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
  · intro B C (h : B * A = C * A)
    refine hA.matrix ?_
    simp only
    rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←
      mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]

Regularity of Matrix from Left-Regularity of Determinant: $\text{IsLeftRegular}(\det A) \Rightarrow \text{IsRegular}(A)$

Informal description

Let $A$ be an $n \times n$ matrix over a commutative ring $\alpha$. If the determinant $\det A$ is left-regular (i.e., $\det A \cdot x = 0$ implies $x = 0$ for all $x \in \alpha$), then $A$ is a regular matrix (both left-regular and right-regular).

Matrix.adjugate_mul_distrib_aux theorem

 (A B : Matrix n n α) (hA : IsLeftRegular A.det) (hB : IsLeftRegular B.det) : adjugate (A * B) = adjugate B * adjugate A

Full source

theorem adjugate_mul_distrib_aux (A B : Matrix n n α) (hA : IsLeftRegular A.det)
    (hB : IsLeftRegular B.det) : adjugate (A * B) = adjugate B * adjugate A := by
  have hAB : IsLeftRegular (A * B).det := by
    rw [det_mul]
    exact hA.mul hB
  refine (isRegular_of_isLeftRegular_det hAB).left ?_
  simp only
  rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
    smul_mul, Matrix.one_mul, mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]

Adjugate of Product of Matrices with Left-Regular Determinants: $\text{adjugate}(AB) = \text{adjugate}(B) \text{adjugate}(A)$

Informal description

For any $n \times n$ matrices $A$ and $B$ over a commutative ring $\alpha$, if the determinants $\det A$ and $\det B$ are left-regular (i.e., $\det A \cdot x = 0$ implies $x = 0$ and similarly for $\det B$), then the adjugate of the product $AB$ equals the product of the adjugates in reverse order: \[ \text{adjugate}(AB) = \text{adjugate}(B) \cdot \text{adjugate}(A). \]

Matrix.adjugate_mul_distrib theorem

(A B : Matrix n n α) : adjugate (A * B) = adjugate B * adjugate A

Full source

/-- Proof follows from "The trace Cayley-Hamilton theorem" by Darij Grinberg, Section 5.3
-/
theorem adjugate_mul_distrib (A B : Matrix n n α) : adjugate (A * B) = adjugate B * adjugate A := by
  let g : Matrix n n α → Matrix n n α[X] := fun M =>
    M.map Polynomial.C + (Polynomial.X : α[X]) • (1 : Matrix n n α[X])
  let f' : MatrixMatrix n n α[X] →+* Matrix n n α := (Polynomial.evalRingHom 0).mapMatrix
  have f'_inv : ∀ M, f' (g M) = M := by
    intro
    ext
    simp [f', g]
  have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M := by
    intro
    rw [RingHom.map_adjugate, f'_inv]
  have f'_g_mul : ∀ M N : Matrix n n α, f' (g M * g N) = M * N := by
    intros M N
    rw [RingHom.map_mul, f'_inv, f'_inv]
  have hu : ∀ M : Matrix n n α, IsRegular (g M).det := by
    intro M
    refine Polynomial.Monic.isRegular ?_
    simp only [g, Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]
  rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←
    adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
    RingHom.map_adjugate, f'_inv, f'_g_mul]

Adjugate of Matrix Product: $\text{adjugate}(AB) = \text{adjugate}(B) \text{adjugate}(A)$

Informal description

For any $n \times n$ matrices $A$ and $B$ over a commutative ring $\alpha$, the adjugate of the product $AB$ equals the product of the adjugates in reverse order: \[ \text{adjugate}(AB) = \text{adjugate}(B) \cdot \text{adjugate}(A). \]

Matrix.adjugate_pow theorem

(A : Matrix n n α) (k : ℕ) : adjugate (A ^ k) = adjugate A ^ k

Full source

@[simp]
theorem adjugate_pow (A : Matrix n n α) (k : ℕ) : adjugate (A ^ k) = adjugate A ^ k := by
  induction k with
  | zero => simp
  | succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]

Adjugate of Matrix Power: $\text{adjugate}(A^k) = (\text{adjugate}\, A)^k$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring $\alpha$ and any natural number $k$, the adjugate of the matrix power $A^k$ equals the $k$-th power of the adjugate of $A$, i.e., \[ \text{adjugate}(A^k) = (\text{adjugate}\, A)^k. \]

Matrix.det_smul_adjugate_adjugate theorem

(A : Matrix n n α) : det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A

Full source

theorem det_smul_adjugate_adjugate (A : Matrix n n α) :
    det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A := by
  have : A * (A.adjugate * A.adjugate.adjugate) =
      A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by
    rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]
  rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,
    Matrix.one_mul] at this

Determinant-Adjugate Identity: $(\det A) \cdot \text{adjugate}(\text{adjugate}(A)) = (\det A)^{n-1} A$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring $\alpha$, the product of the determinant of $A$ with the adjugate of the adjugate of $A$ equals $(\det A)^{n-1}$ times $A$, where $n$ is the size of the matrix. That is, \[ (\det A) \cdot \text{adjugate}(\text{adjugate}(A)) = (\det A)^{n-1} \cdot A. \]

Matrix.adjugate_adjugate theorem

(A : Matrix n n α) (h : Fintype.card n ≠ 1) : adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A

Full source

/-- Note that this is not true for `Fintype.card n = 1` since `1 - 2 = 0` and not `-1`. -/
theorem adjugate_adjugate (A : Matrix n n α) (h : Fintype.cardFintype.card n ≠ 1) :
    adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A := by
  -- get rid of the `- 2`
  rcases h_card : Fintype.card n with _ | n'
  · subsingleton [Fintype.card_eq_zero_iff.mp h_card]
  cases n'
  · exact (h h_card).elim
  rw [← h_card]
  -- express `A` as an evaluation of a polynomial in n^2 variables, and solve in the polynomial ring
  -- where `A'.det` is non-zero.
  let A' := mvPolynomialX n n ℤ
  suffices adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A' by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_mul _)]
  have h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1 := by simp [h_card]
  have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A') := fun x y =>
    mul_left_cancel₀ (det_mvPolynomialX_ne_zero n ℤ)
  apply is_reg.matrix
  simp only
  rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]

Double Adjugate Identity: $\text{adjugate}(\text{adjugate}(A)) = (\det A)^{n-2} A$ for $n \neq 1$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring $\alpha$, where the size $n$ of the matrix is not equal to $1$, the adjugate of the adjugate of $A$ satisfies \[ \text{adjugate}(\text{adjugate}(A)) = (\det A)^{n-2} \cdot A. \]

Matrix.adjugate_adjugate' theorem

(A : Matrix n n α) [Nontrivial n] : adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A

Full source

/-- A weaker version of `Matrix.adjugate_adjugate` that uses `Nontrivial`. -/
theorem adjugate_adjugate' (A : Matrix n n α) [Nontrivial n] :
    adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A :=
  adjugate_adjugate _ <| Fintype.one_lt_card.ne'

Double Adjugate Identity for Nontrivial Matrices: $\text{adjugate}(\text{adjugate}(A)) = (\det A)^{n-2} A$

Informal description

For any $n \times n$ matrix $A$ over a commutative ring $\alpha$, where the index type $n$ is nontrivial (i.e., has more than one element), the adjugate of the adjugate of $A$ satisfies \[ \text{adjugate}(\text{adjugate}(A)) = (\det A)^{n-2} \cdot A. \] Here, $n$ denotes the size of the matrix (the cardinality of the index type).

Mathlib.LinearAlgebra.Matrix.Adjugate

Main definitions

References

Tags