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]
: