charpoly — Mathlib

English

The characteristic polynomial of a linear map f is the same as the characteristic polynomial of its matrix in any basis: (toMatrix b b f).charpoly = f.charpoly.

Русский

Характеристический многочлен отображения f совпадает с характеристическим многочленом его матрицы в любой базе: (toMatrix b b f).charpoly = f.charpoly.

LaTeX

$$$(toMatrix\; b\; b\; f).charpoly = f.charpoly$.$$

Lean4

/-- The characteristic polynomial of `f : M →ₗ[R] M`. -/
def charpoly : R[X] :=
  (toMatrix (chooseBasis R M) (chooseBasis R M) f).charpoly

Похожие утверждения