Topic: Reduction mod m
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?
Bhavik Mehta (May 20 2020 at 17:33):
lemma mod_add_div (m k : ℕ)
: m % k + k * (m / k) = m := in core
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
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
Patrick Massot (May 20 2020 at 17:38):
Well, the real world statement would clearly be in the other direction.
Patrick Massot (May 20 2020 at 17:39):
But library_search will see through that.
Last updated: May 11 2021 at 16:22 UTC