Theorem QuotientGroup.isOpenQuotientMap_mk

Modification history

2024-10-17 02:58

Mathlib/Topology/Algebra/Group/Basic.lean

chore(Topology/Group): move `QuotientGroup` to a new file (#17473)

Modified QuotientGroup.isOpenQuotientMap_mk View on Github →

2024-10-03 16:01

Mathlib/Topology/Algebra/Group/Basic.lean

feat(Topology/Group): drop an unneeded assumption (#16551) …

Added QuotientGroup.isOpenQuotientMap_mk View on Github →