Theorem Con.comapQuotientEquivOfSurj_mk

Modification history

2024-11-04 16:42
Mathlib/GroupTheory/Congruence/Basic.lean
feat(GroupTheory/Congruence): simp lemmas for comap equivalences (#17195) …
Added Con.comapQuotientEquivOfSurj_mkView on Github →