Def Subgroup.commGroupTopologicalClosure

Modification history

2024-11-11 03:06
Mathlib/Topology/Algebra/Group/Basic.lean
chore: change `comm*TopologicalClosure` from `def` to `abbrev` (#18766)
Deleted Subgroup.commGroupTopologicalClosureView on Github →
2023-02-21 20:43
Mathlib/Topology/Algebra/Group/Basic.lean
feat: port Topology.Algebra.Group.Basic (#2267)
Added Subgroup.commGroupTopologicalClosureView on Github →