mccoy's theorem

Stream: Is there code for X?

[Eric Rodriguez]

https://math.stackexchange.com/questions/83121/zero-divisor-in-rx/83171#83171; ctrl+f-fu seems to not find anything but i always fear i don't search in the right generality

[Damiano Testa]

If you did not find this, the argument below might be quick given what is in mathlib.

Suppose that f * g = 0. Invert the leading coefficient of g, and use that if the leading coefficient of a polynomial is a unit, then multiplying by the polynomial only maps to zero the zero polynomial. Thus, f is the zero polynomial in the localisation. It follows that a power of the leading coefficient of g annihilates f.

I believe that most of the steps are in place. However, I am not sure how painful it is to relate inverting the leading coefficient in the ground ring or in a polynomial ring over it.