mem_maxGenEigenspace — Mathlib

English

A vector m lies in maxGenEigenspace μ if and only if there exists k with (f − μ I)^k m = 0.

Русский

Вектор m принадлежит maxGenEigenspace μ тогда и только тогда, когда существует k такой, что (f − μ I)^k m = 0.

LaTeX

$$$m \\in \\maxGenEigenspace(f, \\mu) \\iff \\exists k:\\; ((f - \\mu I)^k) m = 0.$$$

Lean4

@[simp]
theorem mem_maxGenEigenspace (f : End R M) (μ : R) (m : M) :
    m ∈ f.maxGenEigenspace μ ↔ ∃ k : ℕ, ((f - μ • (1 : End R M)) ^ k) m = 0 :=
  mem_genEigenspace_top

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