Commit 2024-02-03 14:26 7509e796

View on Github →

feat: a / c ≡ b / c [PMOD p] (#9619) Also fix a few misported names. From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/ModEq.lean

added theorem AddCommGroup.div_modEq_div

added theorem AddCommGroup.intCast_modEq_intCast'

added theorem AddCommGroup.intCast_modEq_intCast

deleted theorem AddCommGroup.int_cast_modEq_int_cast

added theorem AddCommGroup.natCast_modEq_natCast

deleted theorem AddCommGroup.nat_cast_modEq_nat_cast