isNilpotent_of_isNilpotent — Mathlib

English

If μ is a HasUnifEigenvalue μ 1, then μ belongs to the spectrum of f.

Русский

Если μ является унифицированным собственным значением f при индексе 1, то μ ∈ спектр(f).

LaTeX

$$HasUnifEigenvalue(f, μ, 1) → μ ∈ spectrum(f)$$

Lean4

/-- A nilpotent endomorphism has nilpotent eigenvalues.

See also `LinearMap.isNilpotent_trace_of_isNilpotent`. -/
theorem isNilpotent_of_isNilpotent [NoZeroSMulDivisors R M] {f : End R M} (hfn : IsNilpotent f) {μ : R}
    (hf : f.HasUnifEigenvalue μ 1) : IsNilpotent μ :=
  by
  obtain ⟨m : M, hm⟩ := hf.exists_hasUnifEigenvector
  obtain ⟨n : ℕ, hn : f ^ n = 0⟩ := hfn
  exact ⟨n, by simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n⟩

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