Theorem Con.comapQuotientEquivOfSurj_symm_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_symm_mk'View on Github →