Could Polynomial.decidableDvdMonic be made computable?

Stream: mathlib4

[Daniel Weber]

docs#Polynomial.decidableDvdMonic is noncomputable (while the docs don't show it, it's in a noncomputable section. Is this a problem in docgen?), which is a bit weird for a decidability theorem---is there any purpose to the proof compared to just Classical.dec? Anyway, what would be the best way to make it computable?

[Bolton Bailey]

Seems tricky for this to be made computable when docs#Polynomial.modByMonic is itself noncomputable, computability of polynomials in mathlib is a whole issue, you can see the github wiki page on it.