genEigenspace_zero — Mathlib

English

For any endomorphism f, μ, the 0-th generalized eigenspace is the bottom submodule: genEigenspace μ 0 = ⊥.

Русский

Для любого концевого отображения f, μ нулевое обобщённое собственное пространство равно нижнему подполю: genEigenspace μ 0 = ⊥.

LaTeX

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

Lean4

@[simp]
theorem genEigenspace_zero {f : End R M} {μ : R} : f.genEigenspace μ 0 = ⊥ := by ext; apply mem_genEigenspace_zero

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