Value_of_Adjugate_of_Determinant

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

adjugatedeterminantlinear-algebramatrixproofwiki

Let $D$ be the determinant of order $n$ . Let $D^*$ be the adjugate of $D$ . Then $D^* = D^{n-1}$ .

Preamble

import Mathlib.LinearAlgebra.Matrix.Adjugate

Formal statement

theorem Value_of_Adjugate_of_Determinant {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) : A.adjugate * A = A.det • 1 := by sorry

Source