Theorem AddCommGroup.modEq_iff_zsmul

Modification history

2026-01-16 00:53

Mathlib/Algebra/Group/ModEq.lean

chore(Algebra/ModEq): split file (#34003) …

Modified AddCommGroup.modEq_iff_zsmul View on Github →

2026-01-14 18:34

Mathlib/Algebra/ModEq.lean

refactor(Algebra/ModEq): generalize to monoids (#33849) …

Added AddCommGroup.modEq_iff_zsmul View on Github →