## 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_add and 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 dvd_mul_left)

#### 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