Vector spaces over nontrivially normed fields are perfect spaces #
theorem perfectSpace_of_module (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] :