isNilpotent_iff_charpoly — Mathlib

English

For a nilpotent endomorphism φ, its charpoly equals X^finrank; conversely, if charpoly equals X^finrank, φ is nilpotent.

Русский

Для нильпотентного отображения φ характеристическая полиномия равна X^finrank; наоборот, если полиномия равна X^finrank, то φ нильпотентно.

LaTeX

$$$IsNilpotent(\\phi) \\iff \\operatorname{charpoly}(\\phi) = X^{\\operatorname{finrank} }$$$

Lean4

theorem isNilpotent_iff_charpoly (φ : End R M) : IsNilpotent φ ↔ charpoly φ = X ^ finrank R M :=
  ⟨IsNilpotent.charpoly_eq_X_pow_finrank, fun h ↦ ⟨finrank R M, by rw [← @aeval_X_pow R, ← h, aeval_self_charpoly φ]⟩⟩

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