Zulip Chat Archive

Stream: Is there code for X?

Topic: Simple integer divisibility


view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Oct 26 2020 at 15:45):

I guess not directly, but with a combo of dvd_add and dvd_mul_(left|right) you should be able to get there.

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 15:46):

(let us know if we've said enough)

view this post on Zulip Adam Topaz (Oct 26 2020 at 15:47):

You probably want docs#dvd_mul_of_dvd_left (as opposed to dvd_mul_left)

view this post on Zulip Adam Topaz (Oct 26 2020 at 15:48):

Or docs#dvd_mul_of_dvd_right

view this post on Zulip Johan Commelin (Oct 26 2020 at 15:48):

Oops, "I was always bad with names"

view this post on Zulip 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