English
Under the triangularizable hypothesis, if the generalized eigenspaces cover the space, then there exists μ with HasEigenvalue μ.
Русский
При треугольной оснастке, если суммарные обобщенные эйгенпространства покрывают пространство, существует μ с HasEigenvalue μ.
LaTeX
$$$\\exists μ, f.HasEigenvalue μ$$$
Lean4
/-- In finite dimensions, if the generalized eigenspaces of a linear endomorphism span the whole
space then the same is true of its restriction to any invariant submodule. -/
theorem genEigenspace_restrict_eq_top {p : Submodule K V} {f : Module.End K V} [FiniteDimensional K V] {k : ℕ∞}
(h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ μ, f.genEigenspace μ k = ⊤) :
⨆ μ, Module.End.genEigenspace (LinearMap.restrict f h) μ k = ⊤ :=
by
have := congr_arg (Submodule.comap p.subtype) (Submodule.eq_iSup_inf_genEigenspace k h h')
have h_inj : Function.Injective p.subtype := Subtype.coe_injective
simp_rw [Submodule.inf_genEigenspace f p h, Submodule.comap_subtype_self, ← Submodule.map_iSup,
Submodule.comap_map_eq_of_injective h_inj] at this
exact this.symm
