Theorems · Definition · linear algebra

Matrix.charpoly

{R : Type u_1} → [inst : CommRing R] → {n : Type u_4} → [DecidableEq n] → [Fintype n] → Matrix n n R → Polynomial R

The characteristic polynomial of a matrix M is given by $\det (t I - M)$.

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Cited by

82 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype