Commit 2025-08-11 05:40 0e192ea3

View on Github →

chore(Data/ZMod): golf eq_iff_modEq_nat (#28200) Motivation: Avoid (partial) proof duplication.

Estimated changes

modified theorem ZMod.eq_iff_modEq_nat