minpoly_dvd_charpoly — Mathlib

English

Let M be a square matrix over a field K. Then the minimal polynomial of M divides its characteristic polynomial.

Русский

Пусть M – квадратная матрица над полем K. Тогда минимальный полином матрицы M делит её характеристический полином.

LaTeX

$$$\\minpoly K M \\mid \\mathrm{charpoly}(M)$$$

Lean4

theorem minpoly_dvd_charpoly {K : Type*} [Field K] (M : Matrix n n K) : minpoly K M ∣ M.charpoly :=
  minpoly.dvd _ _ (aeval_self_charpoly M)

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