Theorem AddCommGroup.ModEq.natCast

Modification history

2026-01-16 00:53

Mathlib/Algebra/ModEq.lean

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

Modified AddCommGroup.ModEq.natCast View on Github →

2026-01-14 18:34

Mathlib/Algebra/ModEq.lean

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

Added AddCommGroup.ModEq.natCast View on Github →