Theorems · Theorem · linear algebra

Matrix.det_smul_adjugate_adjugate

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

Defined in

Mathlib.LinearAlgebra.Matrix.Adjugate

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommRing