English
A weaker form of the adjugate-adjugate identity holds for any nontrivial size: adj(adj(A)) = det(A)^(n−2) · A.
Русский
Слабая форма тождества adj(adj(A)) = det(A)^(n−2) · A справедлива для любого ненулевого размера матрицы.
LaTeX
$$$\\operatorname{adj}(\\operatorname{adj}(A)) = \\det(A)^{(n-2)} \\cdot A$$$
Lean4
/-- 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'