Stream: Is there code for X?
Topic: Simple integer divisibility
Meyer Zinn (Oct 26 2020 at 15:43):
Hello, novice user here. Is there any quick theorem for a | b -> a | c -> forall w x, a | wb + xc? (i.e., divisibility of linear combinations)
Kevin Buzzard (Oct 26 2020 at 15:45):
That looks to me like an easy consequence of two theorems which are probably there:
a | b -> a | w*b and
a | b -> a | c -> a | (b+c)
Johan Commelin (Oct 26 2020 at 15:45):
I guess not directly, but with a combo of
dvd_mul_(left|right) you should be able to get there.
Kevin Buzzard (Oct 26 2020 at 15:46):
(let us know if we've said enough)
Adam Topaz (Oct 26 2020 at 15:47):
You probably want docs#dvd_mul_of_dvd_left (as opposed to
Adam Topaz (Oct 26 2020 at 15:48):
Johan Commelin (Oct 26 2020 at 15:48):
Oops, "I was always bad with names"
Meyer Zinn (Oct 27 2020 at 14:53):
Thanks for the help! Don't know why those eluded me for so long.
Last updated: May 17 2021 at 14:12 UTC