Quotient Remainder Theorem

Stream: Is there code for X?

[Zeyi Zhao]

Hi everyone, could anybody remind me where I could find the quotient reminder theorem over Q[x] in the mathlib repo? Thanks!

[Notification Bot]

This topic was moved here from #general > Quotient Reminder Theorem by Yury G. Kudryashov.

[Yury G. Kudryashov]

Please post a #mwe with a theorem you want to prove.

[Yury G. Kudryashov]

Also, what did you do to find it yourself?

[Zeyi Zhao]

What I am trying to prove is that given a polynomial p(x) with rational coefficients, it can be uniquely written as p(x)=q(x)f(x)+r(x), where f(x) is given, q(x) is the quotient, and r(x) is the remainder. Since I am pretty new to it, I am doing a primary search for explicit theorems over the repos. It is really helpful if you could tell me which repo I should be looking at to start with.

[Johan Commelin]

docs#Polynomial.instEuclideanDomain gives you the "euclidean algorithm" for polynomial rings

[Zeyi Zhao]

Johan Commelin said:

docs#Polynomial.instEuclideanDomain gives you the "euclidean algorithm" for polynomial rings

Thanks very much for the help!

[Kevin Buzzard]

Usually these theorems are called quot_add_rem but it would help if you asked the exact question in lean