Theorems · Theorem · linear algebra

Matrix.adjugate_adjugate

∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  Fintype.card n ≠ 1 → A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A

Note that this is not true for Fintype.card n = 1 since 1 - 2 = 0 and not -1.

Defined in

Mathlib.LinearAlgebra.Matrix.Adjugate

Cited by

1 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeCommRing