Theorems · Definition · linear algebra

Matrix.charpoly.univ

(R : Type u_1) →
  (n : Type u_3) → [inst : CommRing R] → [Fintype n] → [DecidableEq n] → Polynomial (MvPolynomial (n × n) R)

The universal characteristic polynomial for n × n-matrices, is the characteristic polynomial of Matrix.mvPolynomialX n n ℤ with entries Xᵢⱼ. Its i-th coefficient is a homogeneous polynomial of degree n - i, see Matrix.charpoly.univ_coeff_isHomogeneous. By evaluating the coefficients at the entries of a matrix M, one obtains the characteristic polynomial of M, see Matrix.charpoly.univ_map_eval₂Hom.

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommRingFintypeDecidableEq