Zulip Chat Archive

Stream: Is there code for X?

Topic: Degree of the remainder of polynomial division


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

view this post on Zulip Heather Macbeth (Oct 25 2020 at 03:02):

Is this docs#euclidean_domain.mod_lt ?

view this post on Zulip Patrick Lutz (Oct 25 2020 at 03:28):

Ohh, I think so! Thanks!


Last updated: May 07 2021 at 19:12 UTC