Matrix adjugation

This file records dimension-independent consequences of the standard matrix adjugate identities.

@[simp]

theorem Matrix.adjugate_mul_self_eq_one_iff_det_eq_one {K : Type u_1} [CommRing K] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n K) : A.adjugate * A = 1 ↔ A.det = 1

For a square matrix with finite indices, the left adjugate equation is equivalent to determinant one.