Commit 2026-07-10 20:06 e0394640

View on Github →

feat: more API specific to strict group homs (#41238)

Move the section of Topology.Maps.Strict.Basic about group homs to a new file Topology.Maps.Strict.Group
add more criterions for strictness of group homs
the first isomorphism theorem holds for strict group homs, yielding a ContinuousMulEquiv
various tweaks to namespaces and variables throughout the two files.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Maps/Strict/Basic.lean

added theorem Homeomorph.comp_isStrictMap_iff

added theorem Homeomorph.isStrictMap_comp_iff

added theorem IsClosedMap.isStrictMap

added theorem IsHomeomorph.isStrictMap

added theorem IsOpenMap.isStrictMap

deleted theorem MonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict

deleted theorem MonoidHom.isStrictMap_prodMap

deleted theorem MonoidHom.isStrictMap_prodMap_iff

deleted theorem Topology.Homeomorph.comp_isStrictMap_iff

deleted theorem Topology.Homeomorph.isStrictMap_comp_iff

deleted theorem Topology.IsClosedMap.isStrictMap

deleted theorem Topology.IsHomeomorph.isStrictMap

deleted theorem Topology.IsOpenMap.isStrictMap

Created Mathlib/Topology/Maps/Strict/Group.lean