Commit 2025-09-16 23:57 f463d1b5

View on Github →

chore: TopologicalGroup.isOpenMap_iff_nhds_one -> IsTopologicalGroup.isOpenMap_iff_nhds_one (#29721)

Estimated changes

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem IsTopologicalGroup.isOpenMap_iff_nhds_one

deleted theorem TopologicalGroup.isOpenMap_iff_nhds_one

Modified Mathlib/Topology/Algebra/IsOpenUnits.lean