Commit 2025-02-11 07:39 751f9504

View on Github →

feat(Topology/Algebra): monoids with open units (#21298)

Estimated changes

Modified Mathlib.lean

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

added theorem TopologicalGroup.isOpenMap_iff_nhds_one

Created Mathlib/Topology/Algebra/IsOpenUnits.lean

added theorem IsOpenUnits.of_isAdic