charpoly_monic — Mathlib

English

For a linear map f over a field K on a finite-dimensional space, the minimal polynomial minpoly_K f divides the characteristic polynomial f.charpoly.

Русский

Для отображения f над полем K на конечномерном пространстве минимальный многочлен minpoly_K f делит характеристический многочлен f.charpoly.

LaTeX

$$minpoly K f ∣ f.charpoly$$

Lean4

theorem charpoly_monic : f.charpoly.Monic :=
  Matrix.charpoly_monic _

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