mem_genEigenspace_zero — Mathlib

English

For any endomorphism f of an R-module M and any μ ∈ R, the 0-th generalized eigenspace of f at μ consists only of the zero vector; equivalently, f.genEigenspace μ 0 = ⊥ and hence x ∈ f.genEigenspace μ 0 implies x = 0.

Русский

Для любого концевого отображения f на модуле M над кольцом R и для любого μ ∈ R нулое обобщённое собственное пространство f относительно μ состоит только из нулевого вектора; то есть f.genEigenspace μ 0 = ⊥, следовательно x ∈ f.genEigenspace μ 0 тогда и только тогда, что x = 0.

LaTeX

$$$f\,\mathrm{genEigenspace}(\mu, 0) = \bot$$$

Lean4

theorem mem_genEigenspace_zero {f : End R M} {μ : R} {x : M} : x ∈ f.genEigenspace μ 0 ↔ x = 0 := by
  rw [← Nat.cast_zero, mem_genEigenspace_nat, pow_zero, LinearMap.mem_ker, Module.End.one_apply]

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