Commit 2026-01-14 18:34 8fa4ee3d

View on Github →

refactor(Algebra/ModEq): generalize to monoids (#33849) Generalize the definition of AddCommGroup.ModEq to AddCommMonoids. Also, no longer @[expose] the definition, since the precise definitional equality is not important. Adds:

  • AddCommGroup.ModEq.map
  • AddCommGroup.instSymmModEq
  • AddCommGroup.map_modEq_iff
  • AddCommGroup.modEq_iff_natModEq
  • AddCommGroup.modEq_iff_nsmul
  • AddCommGroup.modEq_iff_zsmul
  • AddCommGroup.modEq_iff_zsmul' Moves
  • AddCommGroup.modEq_iff_int_modEq -> AddCommGroup.modEq_iff_intModEq

Estimated changes

added theorem AddCommGroup.ModEq.map
deleted theorem AddCommGroup.ModEq.trans
modified def AddCommGroup.ModEq
modified theorem AddCommGroup.add_modEq_left
modified theorem AddCommGroup.modEq_comm
modified theorem AddCommGroup.modEq_refl
modified theorem AddCommGroup.modEq_sub
modified theorem AddCommGroup.modEq_zero
modified theorem toIcoMod_inj