FROBENIUS: Fields of fractions of integral extensions are algebraic

[kbuzzard]

If $S/R$ is an integral extension of (commutative) integral domains with field of fractions $L/K$ then $L/K$ is algebraic. The proof uses the fact (proved in another issue) that if $s\in S$ is nonzero then it divides a nonzero element of $r$, to "clear denominators". More precisely, if $n/d\in L$ then choose $d\in R$ rather than $S$ using the previous issue, and then scale the min poly of $n\in A[X]$ appropriately. This is f_exists in FrobeniusRiou.lean . At the time of writing I am a bit confused because this proof doesn't seem to be used in Bourbaki52222.algebraic but that proof also appears to use sorry somewhere.

In fact we need a stronger theorem: if every element of S is annihilated by a monic polynomial of some fixed degree n then this is also true for every element of L.

The key definition here is residueFieldExtensionPolynomial, which is currently stubbed out (with an incorrect definition). The definition should be the "scaling up" definition.

[AlexBrodbelt]

I will work on this

[kbuzzard]

Frobenius elements are now on their way to mathlib in leanprover-community/mathlib4#17717 and in particular the sorry corresponding to this task is filled. Hence this task can be considered completed.