Theorems · Theorem · linear algebra

Matrix.coeff_det_one_add_X_smul_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 : ℕ),
  (1 + Polynomial.X • M.map ⇑Polynomial.C).det.coeff k =
    ∑ s ∈ Finset.powersetCard k Finset.univ, (M.submatrix Subtype.val Subtype.val).det

The k-th coefficient of det (1 + X • M) equals the sum of all k×k principal minors of M. This generalizes coeff_det_one_add_X_smul_one (the k = 1 case, which gives the trace) and det_eq_sign_charpoly_coeff (the k = n case, which gives the determinant).

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype