Commit 2026-06-19 19:19 1220aa60

View on Github →

refactor: make {Con,AddCon,RingCon}.congr match Quotient.congr (#40819) This adds an explicit equivalence argument, rather than defaulting it to refl. Also adds a missing symm lemma for each.

Estimated changes

Modified Mathlib/GroupTheory/Congruence/Basic.lean

modified theorem Con.congr_mk

added theorem Con.congr_symm

Modified Mathlib/RingTheory/Congruence/Hom.lean

modified theorem RingCon.congr_mk

added theorem RingCon.congr_symm

modified theorem RingCon.congrₐ_mk

added theorem RingCon.congrₐ_symm