Zulip Chat Archive

Stream: maths

Topic: Reduction mod m


view this post on Zulip Patrick Stevens (May 20 2020 at 17:32):

For the life of me I can't find lemma reduce_mod (m n : nat) : (n / m) * m + (n % m) = n := by sorry, and it absolutely has to be somewhere. library_search gives me nothing; no variant on "div_mul" or "div_mod" or "division_alg" that I've tried has given me anything. Can someone point me to it?

view this post on Zulip Bhavik Mehta (May 20 2020 at 17:33):

There's lemma mod_add_div (m k : ℕ) : m % k + k * (m / k) = m := in core

view this post on Zulip Patrick Massot (May 20 2020 at 17:36):

It's annoying to have a hard time finding this. Should we have variants? I guess there are four possibilities, excluding the eq.symm variations

view this post on Zulip Patrick Stevens (May 20 2020 at 17:38):

Excluding the symm variations seems correct; I would hardly expect a lemma to go from simple to more complex

view this post on Zulip Patrick Massot (May 20 2020 at 17:38):

Well, the real world statement would clearly be in the other direction.

view this post on Zulip Patrick Massot (May 20 2020 at 17:39):

But library_search will see through that.


Last updated: May 11 2021 at 16:22 UTC