## Stream: Is there code for X?

### Topic: Degree of the remainder of polynomial division

#### Patrick Lutz (Oct 25 2020 at 02:56):

Is there anything in mathlib saying that if p and q are polynomials (with q nonzero) then the degree of p % q is less than the degree of q? It seems like this must be in mathlib, but somehow I can only find it stated for monic polynomials (in data.polynomial.div).

#### Heather Macbeth (Oct 25 2020 at 03:02):

Is this docs#euclidean_domain.mod_lt ?

#### Patrick Lutz (Oct 25 2020 at 03:28):

Ohh, I think so! Thanks!

Last updated: May 07 2021 at 19:12 UTC