charpoly_natDegree — Mathlib

English

For a linear map f with appropriate finiteness assumptions, the natDegree of f.charpoly equals finrank_R M.

Русский

При подходящих условиях конечности natDegree(f.charpoly) равен finrank_R M.

LaTeX

$$natDegree (f.charpoly) = finrank R M$$

Lean4

theorem charpoly_natDegree [Nontrivial R] [StrongRankCondition R] : natDegree (charpoly f) = finrank R M := by
  rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]

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