adjugate_mul — Mathlib

English

For any square matrix A, the adjugate satisfies adj(A) · A = det(A) I_n.

Русский

Для любой квадратной матрицы A выполняется adj(A) · A = det(A) I_n.

LaTeX

$$\n$\operatorname{adj}(A) \; A = \det(A) \; I_n$$$

Lean4

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]

Похожие утверждения