charpoly_def — Mathlib

English

The characteristic polynomial of f is defined to be the characteristic polynomial of its matrix in any basis.

Русский

Характеристический многочлен f определяется как характеристический многочлен его матрицы в любой базе.

LaTeX

$$f.charpoly = (toMatrix (chooseBasis R M) (chooseBasis R M) f).charpoly$$

Lean4

theorem charpoly_def : f.charpoly = (toMatrix (chooseBasis R M) (chooseBasis R M) f).charpoly :=
  rfl

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