Theorems · Definition · linear algebra

Matrix.adjugate

{n : Type v} → {α : Type w} → [DecidableEq n] → [Fintype n] → [CommRing α] → Matrix n n α → Matrix n n α

The adjugate matrix is the transpose of the cofactor matrix. Typically, the cofactor matrix is defined by taking minors, i.e. the determinant of the matrix with a row and column removed. However, the proof of mul_adjugate becomes a lot easier if we use the matrix replacing a column with a basis vector, since it allows us to use facts about the cramer map.

Defined in

Mathlib.LinearAlgebra.Matrix.Adjugate

Cited by

64 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommRing