Additional results on topological groups

A result on topological groups that has been separated out as it requires more substantial imports developing positive compacts.

theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (K : PositiveCompacts G) : LocallyCompactSpace G

Every topological group in which there exists a compact set with nonempty interior is locally compact.

theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup {G : Type u} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (K : PositiveCompacts G) : LocallyCompactSpace G

Every topological additive group in which there exists a compact set with nonempty interior is locally compact.