Zulip Chat Archive
Stream: lean4
Topic: Integer division
Ruben Van de Velde (Dec 11 2022 at 19:18):
Did the definition of integer division change? I'm getting a seemingly unprovable goal in
protected theorem add_mul_div_right (a b : ℤ) {c : ℤ} (H : c ≠ 0) : (a + b * c) / c = a / c + b
Reid Barton (Dec 11 2022 at 19:39):
Yes, it did
Mauricio Collares (Dec 11 2022 at 19:39):
C-style truncating division is so unintuitive
Mauricio Collares (Dec 11 2022 at 19:40):
https://blog.vero.site/post/modulo is a fun read, though
Reid Barton (Dec 11 2022 at 20:07):
Last updated: Dec 20 2023 at 11:08 UTC