Theorem Con.congr_mk

Modification history

2026-06-19 19:19
Mathlib/GroupTheory/Congruence/Basic.lean
refactor: make `{Con,AddCon,RingCon}.congr` match `Quotient.congr` (#40819) …
Modified Con.congr_mkView on Github →
2024-11-04 16:42
Mathlib/GroupTheory/Congruence/Basic.lean
feat(GroupTheory/Congruence): simp lemmas for comap equivalences (#17195) …
Added Con.congr_mkView on Github →