isNilpotent_of_isNilpotent — Mathlib

English

A nilpotent endomorphism has nilpotent eigenvalues.

Русский

Нильпотентный эндоморфизм имеет нильпотентные собственные значения.

LaTeX

$$IsNilpotent f ⇒ IsNilpotent μ for any μ in spectrum(f).$$

Lean4

/-- A nilpotent endomorphism has nilpotent eigenvalues.

See also `LinearMap.isNilpotent_trace_of_isNilpotent`. -/
nonrec theorem isNilpotent_of_isNilpotent [NoZeroSMulDivisors R M] {f : End R M} (hfn : IsNilpotent f) {μ : R}
    (hf : f.HasEigenvalue μ) : IsNilpotent μ :=
  hf.isNilpotent_of_isNilpotent hfn

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