Zulip Chat Archive
Stream: mathlib4
Topic: Int division, again
Ruben Van de Velde (Jan 16 2023 at 10:10):
We have
#align int.mod_eq_of_lt Int.mod_eq_of_ltₓ
when there's a perfectly good Int.emod_eq_of_lt that's about % as used in mathlib. Should we change that? How about the others nearby?
Last updated: May 02 2025 at 03:31 UTC