theorem Subgroup.dense_iff_topologicalClosure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Subgroup G} : Dense ↑s ↔ s.topologicalClosure = ⊤

A subgroup of a topological group is dense if and only if its topological closure is the entire group.

theorem AddSubgroup.dense_iff_topologicalClosure_eq_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {s : AddSubgroup G} : Dense ↑s ↔ s.topologicalClosure = ⊤

An additive subgroup of a topological group is dense if and only if its topological closure is the entire group.