Commit 2025-06-26 10:20 853b1aa0

View on Github →

refactor(Algebra/ModEq): more symmetric lemma statements (#26414) This keeps the variables in the same order on both sides. Also adds a trivial lemma about 0.

Estimated changes

Modified Mathlib/Algebra/ModEq.lean

modified theorem AddCommGroup.modEq_iff_eq_mod_zmultiples

added theorem AddCommGroup.modEq_zero_iff_eq_zsmul

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

modified theorem toIcoMod_inj

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean