Theorems · Theorem · linear algebra

Matrix.charpoly_coeff_eq_sum_minors

∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  ∀ k ≤ Fintype.card n,
    M.charpoly.coeff (Fintype.card n - k) =
      (-1) ^ k * ∑ s ∈ Finset.powersetCard k Finset.univ, (M.submatrix Subtype.val Subtype.val).det

The coefficients of the characteristic polynomial are signed sums of principal minors. Specifically, the (n-k)-th coefficient of the characteristic polynomial of M equals (-1)^k times the sum of all k×k principal minors of M.

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype