Theorems · Theorem · linear algebra

Matrix.det_one_add_X_smul

∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  (1 + Polynomial.X • M.map ⇑Polynomial.C).det =
    1 + M.trace • Polynomial.X + (1 + Polynomial.X • M.map ⇑Polynomial.C).det.divX.divX * Polynomial.X ^ 2

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype