Commit 2026-06-19 09:20 189bef07

View on Github →

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

Estimated changes

Modified Mathlib/Data/Setoid/Basic.lean

added theorem Setoid.coe_map_of_ker_le

added theorem Setoid.comap_comp

added theorem Setoid.comap_id

added theorem Setoid.comap_injective

added theorem Setoid.comap_map_eq

added theorem Setoid.comap_map_of_ker_le

added theorem Setoid.comap_rel_eq

added theorem Setoid.comap_surjective

added theorem Setoid.ker_eq_bot_iff

added theorem Setoid.le_comap_map

added theorem Setoid.le_iff_rel_le

Modified Mathlib/GroupTheory/Congruence/Basic.lean

deleted theorem Con.le_comap_conGen

Modified Mathlib/GroupTheory/Congruence/Defs.lean

added theorem Con.comap_comp

added theorem Con.comap_id

added theorem Con.comap_injective

added theorem Con.le_comap_conGen

Modified Mathlib/RingTheory/Congruence/Basic.lean

added theorem RingCon.comap_injective

modified theorem RingCon.comap_mono

added theorem RingCon.comap_ringConGen_ringEquiv

added theorem RingCon.le_comap_ringConGen

Modified Mathlib/RingTheory/Congruence/Defs.lean

added theorem RingCon.comap_nonUnitalRingHomComp

added theorem RingCon.comap_nonUnitalRingHomId

added theorem RingCon.comap_ringHomComp

added theorem RingCon.comap_ringHomId