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):

https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/.5BRFC.5D.20Int.2Ediv.20convention/near/296956937


Last updated: Dec 20 2023 at 11:08 UTC