@[simp]

theorem ContinuousLinearMap.range_zero {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type u_3) (M₂ : Type u_4) [TopologicalSpace M] [AddCommMonoid M] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] [RingHomSurjective σ] : LinearMap.range 0 = ⊥

@[simp]

theorem ContinuousLinearMap.ker_zero {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type u_3) (M₂ : Type u_4) [TopologicalSpace M] [AddCommMonoid M] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] : LinearMap.ker 0 = ⊤

theorem ContinuousLinearMap.ker_mk {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type u_3) (M₂ : Type u_4) [TopologicalSpace M] [AddCommMonoid M] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] (f : M →ₛₗ[σ] M₂) (hf : Continuous f.toFun) : LinearMap.ker { toLinearMap := f, cont := hf } = LinearMap.ker f

theorem ContinuousLinearMap.support_eq_sup_eigenspace_nonzero {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [RCLike 𝕜] (A : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) (hA : (↑A).IsSymmetric) : LinearMap.range A = ⨆ (μ : 𝕜), ⨆ (_ : μ ≠ 0), Module.End.eigenspace (↑A) μ

The support of a Hermitian matrix is the sum of its nonzero eigenspaces.