Theorem QuotientGroup.dense_image_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.dense_image_mk View on Github →

2024-09-06 08:34

Mathlib/Topology/Algebra/Group/Basic.lean

feat(Topology/Group): add `QuotientGroup.dense{pre,}image_mk` (#15576)

Added QuotientGroup.dense_image_mk View on Github →