Theorem Con.le_comap_conGen

Modification history

2026-06-19 09:20

Mathlib/GroupTheory/Congruence/Basic.lean

feat: more lemmas about `{Setoid,Con,AddCon,RingCon}.comap` (#40697)

Modified Con.le_comap_conGen View on Github →

2024-11-04 16:42

Mathlib/GroupTheory/Congruence/Basic.lean

feat(GroupTheory/Congruence): simp lemmas for comap equivalences (#17195) …

Added Con.le_comap_conGen View on Github →