charpoly_zero — Mathlib

English

For the zero endomorphism on a finite-dimensional module, its characteristic polynomial is X^finrank.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem charpoly_zero [StrongRankCondition R] : (0 : M →ₗ[R] M).charpoly = X ^ Module.finrank R M := by
  simp [charpoly, Module.finrank_eq_card_chooseBasisIndex]

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