∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (S : Submodule R M) [IsTopologicalAddGroup M], IsTopologicalAddGroup (M ⧸ S)