Theorems · Definition · linear algebra

Matrix.charmatrix

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

The "characteristic matrix" of M : Matrix n n R is the matrix of polynomials $t I - M$. The determinant of this matrix is the characteristic polynomial.

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Cited by

42 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype