hex

3.3. Cofactor expansion🔗

Deleting one row and one column gives a minor. The signed minor is a cofactor, and the determinant is the alternating sum of entries against their cofactors along any fixed row or column.

🔗def
Hex.Matrix.deleteRowCol.{u} {R : Type u} {n : Nat}
  (M : Hex.Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) :
  Hex.Matrix R n n
Hex.Matrix.deleteRowCol.{u} {R : Type u}
  {n : Nat}
  (M : Hex.Matrix R (n + 1) (n + 1))
  (row col : Fin (n + 1)) :
  Hex.Matrix R n n

Delete one row and one column from an (n + 1) × (n + 1) matrix.

🔗def
Hex.Matrix.cofactorSign.{u} {R : Type u} [OfNat R 1] [Neg R] {n : Nat}
  (row col : Fin (n + 1)) : R
Hex.Matrix.cofactorSign.{u} {R : Type u}
  [OfNat R 1] [Neg R] {n : Nat}
  (row col : Fin (n + 1)) : R

The alternating sign used in signed cofactors.

🔗def
Hex.Matrix.cofactor.{u} {R : Type u} [Lean.Grind.Ring R] {n : Nat}
  (M : Hex.Matrix R (n + 1) (n + 1)) (row col : Fin (n + 1)) : R
Hex.Matrix.cofactor.{u} {R : Type u}
  [Lean.Grind.Ring R] {n : Nat}
  (M : Hex.Matrix R (n + 1) (n + 1))
  (row col : Fin (n + 1)) : R

The signed cofactor for the local Leibniz determinant.

🔗theorem
Hex.Matrix.det_eq_foldl_laplace_row.{u} {R : Type u}
  [Lean.Grind.CommRing R] {n : Nat} (M : Hex.Matrix R (n + 1) (n + 1))
  (row : Fin (n + 1)) :
  M.det =
    List.foldl (fun acc col => acc + M[row][col] * M.cofactor row col) 0
      (List.finRange (n + 1))
Hex.Matrix.det_eq_foldl_laplace_row.{u}
  {R : Type u} [Lean.Grind.CommRing R]
  {n : Nat}
  (M : Hex.Matrix R (n + 1) (n + 1))
  (row : Fin (n + 1)) :
  M.det =
    List.foldl
      (fun acc col =>
        acc +
          M[row][col] *
            M.cofactor row col)
      0 (List.finRange (n + 1))

Laplace expansion of the determinant along an arbitrary fixed row.