FROBENIUS: elements of top ring divide elements of bottom ring

[kbuzzard]

If $R$ is a commutative ring and $S$ is a commutative $R$-algebra which is integral over $R$, and if $S$ is an integral domain, then I claim that for every nonzero element $s$ of $S$ there's a nonzero element of $r$ such that $s$ divides the image of $r$ in $S$.

The proof of this seems straightforward and I wonder if we already have it in mathlib (it should probably be PRed directly). It goes like this. WLOG the map from $R$ to $S$ is injective. if $s\in S$ then choose some monic poly in $R[X]$ which annihilates $s$. This polynomial cannot be of the form $X^n$ because $s\not=0$ and $S$ is an integral domain. Hence it is of the form $X^n+...+rX^d$ with $d<n$ and $r\neq0$. Again using the fact that $S$ is an ID we deduce that there's a monic polynomial with nonzero constant term which annihilates $b$ (namely $X^{n-d}+...+r$) and $r$ is easily seen to work.

[morrison-daniel]

I will work on this

[morrison-daniel]

Completed in PR #157