Commit 2023-09-12 12:40 21f843c8

View on Github →

chore (RingTheory.Congruence): make RingCon extend AddCon and Con (#6772) Currently RingCon extends Add and Mul. This changes it to extend AddCon and Con directly.

Estimated changes

Modified Mathlib/RingTheory/Congruence.lean

modified theorem RingCon.rel_mk

deleted def RingCon.toAddCon

deleted def RingCon.toCon

added theorem RingCon.toCon_coe_eq_coe

modified structure RingCon

modified def ringConGen