Eigenspaces of continuous linear maps

This file provides some basic properties of eigenspaces of continuous linear maps.

These results are in a separate file to avoid heavy topology imports.

instance ContinuousLinearMap.isClosed_genEigenspace {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [T0Space M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] (f : M →L[R] M) (μ : R) (n : ℕ) : IsClosed ↑((Module.End.genEigenspace (↑f) μ) ↑n)

instance ContinuousLinearMap.isClosed_eigenspace {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [T0Space M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] (f : M →L[R] M) (μ : R) : IsClosed ↑(Module.End.eigenspace (↑f) μ)