mem_genEigenspace_one — Mathlib

English

An element x lies in the one-exponent generalized eigenspace iff f x = μ x.

Русский

Элемент x принадлежит обобщённому пространству степени 1 тогда и только тогда, когда f x = μ x.

LaTeX

$$$$ x \\in f.genEigenspace\\, μ\\, 1 \\;\\Leftrightarrow\\; f(x) = μ \\cdot x. $$$$

Lean4

@[simp]
theorem mem_genEigenspace_one {f : End R M} {μ : R} {x : M} : x ∈ f.genEigenspace μ 1 ↔ f x = μ • x := by
  rw [genEigenspace_one, LinearMap.mem_ker, LinearMap.sub_apply, sub_eq_zero, LinearMap.smul_apply,
    Module.End.one_apply]
    -- `simp` can prove this using `genEigenspace_zero`

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