Commit 2026-06-24 10:56 cd4c002e

View on Github →

feat: API and proof of isStrictMap_prodMap (#38937)

Estimated changes

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

added theorem MonoidHom.isOpenQuotientMap_iff_isQuotientMap

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

added theorem MonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict

added theorem MonoidHom.isStrictMap_prodMap

added theorem Topology.Homeomorph.comp_isStrictMap_iff

added theorem Topology.Homeomorph.isStrictMap_comp_iff