charpoly_natDegree_eq_dim — Mathlib

English

For a matrix M over a commutative ring, the degree of its characteristic polynomial equals the dimension card(n).

Русский

Степень характерполиома матрицы M равна размерности card(n).

LaTeX

$$$$ \\deg(\\operatorname{charpoly}(M)) = |n|. $$$$

Lean4

@[simp]
theorem charpoly_natDegree_eq_dim [Nontrivial R] (M : Matrix n n R) : M.charpoly.natDegree = Fintype.card n :=
  natDegree_eq_of_degree_eq_some (charpoly_degree_eq_dim M)

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