Compact operators and finite dimensional spaces

This file contains results linking IsCompactOperator with FiniteDimensional.

The motivation for not including this in the same file as the definition of compact operators is that Mathlib.Topology.Algebra.Module.FiniteDimension is quite a heavy import to add there.

theorem isCompactOperator_id_iff_finiteDimensional {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyCompactSpace 𝕜] : IsCompactOperator id ↔ FiniteDimensional 𝕜 E

theorem FiniteDimensional.of_isCompactOperator_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [T2Space E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] (h : IsCompactOperator id) : FiniteDimensional 𝕜 E

If the identity operator of a Banach space over a nontrivially normed field is compact, then the space is finite dimensional.