Commit 2024-09-06 08:34 49c7342a

View on Github →

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

Estimated changes

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

added theorem QuotientGroup.dense_image_mk

added theorem QuotientGroup.dense_preimage_mk