∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] [CompactSpace R]
  [Module.Finite R M], CompactSpace M