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: Dec 20 2023 at 11:08 UTC