Theorems · Definition · linear algebra

Matrix.charpolyRev

{R : Type u} → [inst : CommRing R] → {n : Type v} → [DecidableEq n] → [Fintype n] → Matrix n n R → Polynomial R

The reverse of the characteristic polynomial of a matrix. It has some advantages over the characteristic polynomial, including the fact that it can be extended to infinite dimensions (for appropriate operators). In such settings it is known as the "characteristic power series".

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype