Theorem Submonoid.map_comap_eq_self_of_surjective

Modification history

2025-04-30 10:47
Mathlib/Algebra/Group/Submonoid/Operations.lean
feat(QuotientGroup): surjectivity and kernel of `QuotientGroup.map` (#23205) …
Added Submonoid.map_comap_eq_self_of_surjectiveView on Github →