adjugate_adjugate' — Mathlib

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'

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