Theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_Group

Modification history

2023-05-31 10:33
Mathlib/Topology/Algebra/Group/Compact.lean
feat: port MeasureTheory.Measure.Haar.Basic (#4517) …
Deleted TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_GroupView on Github →
2023-02-21 23:06
Mathlib/Topology/Algebra/Group/Compact.lean
feat: Port/Topology.Algebra.Group.Compact (#2420)
Added TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_GroupView on Github →