Commit 2026-01-16 00:53 721b21cf

View on Github →

chore(Algebra/ModEq): split file (#34003) Minor modifications to the lemmas linking it to Nat.ModEq and Int.ModEq to make the proofs work, otherwise copy+paste+add stub module docs.

Estimated changes

added theorem AddCommGroup.ModEq.map
added theorem AddCommGroup.modEq_neg
added theorem AddCommGroup.modEq_rfl
added theorem AddCommGroup.modEq_sub
deleted theorem AddCommGroup.ModEq.map
deleted def AddCommGroup.ModEq
deleted theorem AddCommGroup.modEq_comm
deleted theorem AddCommGroup.modEq_neg
deleted theorem AddCommGroup.modEq_refl
deleted theorem AddCommGroup.modEq_rfl
deleted theorem AddCommGroup.modEq_sub
deleted theorem AddCommGroup.modEq_zero
modified def Int.ModEq
modified def Nat.ModEq