hex

3.4. The adjugate🔗

The adjugate is the transpose of the cofactor matrix. Its defining identity, M * adjugate M = det M • identity, is what Cramer's rule rests on. Over a commutative ring it holds without any invertibility hypothesis.

🔗def
Hex.Matrix.adjugate.{u} {R : Type u} [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R (n + 1) (n + 1)) : Hex.Matrix R (n + 1) (n + 1)
Hex.Matrix.adjugate.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R (n + 1) (n + 1)) :
  Hex.Matrix R (n + 1) (n + 1)

The local adjugate matrix: entry (i, j) is the cofactor at row j, column i of M. This is the transpose of the cofactor matrix.

🔗theorem
Hex.Matrix.mul_adjugate.{u} {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat} (M : Hex.Matrix R (n + 1) (n + 1)) :
  M * M.adjugate = M.det • Hex.Matrix.identity (n + 1)
Hex.Matrix.mul_adjugate.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat}
  (M : Hex.Matrix R (n + 1) (n + 1)) :
  M * M.adjugate =
    M.det • Hex.Matrix.identity (n + 1)

The adjugate identity M * adjugate M = det M • identity.