charpoly_one — Mathlib

English

For the identity endomorphism on a finite-dimensional module, its characteristic polynomial is (X-1)^{finrank}.

Русский

Для единичного отображения характеристический многочлен равен (X-1)^{finrank}.

LaTeX

$$(1: M → M).charpoly = (X - 1)^{\operatorname{finrank} R M}$$

Lean4

theorem charpoly_one [StrongRankCondition R] : (1 : M →ₗ[R] M).charpoly = (X - 1) ^ Module.finrank R M := by
  simp [charpoly, Module.finrank_eq_card_chooseBasisIndex, Matrix.charpoly_one]

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