Ax-Grothendieck for algebraic extensions of ZMod p

This file proves that if R is an algebraic extension of a finite field, then any injective polynomial map R^n → R^n is also surjective.

This proof is required for the true Ax-Grothendieck theorem, which proves the same result for any algebraically closed field of characteristic zero.

TODO

The proof of the theorem for characteristic zero is not in mathlib, but it is at https://github.com/Jlh18/ModelTheoryInLean8

theorem ax_grothendieck_of_locally_finite {ι : Type u_1} {K : Type u_2} {R : Type u_3} [Field K] [Finite K] [CommRing R] [Finite ι] [Algebra K R] (alg : Algebra.IsAlgebraic K R) (ps : ι → MvPolynomial ι R) (hinj : Function.Injective fun (v : ι → R) (i : ι) => (MvPolynomial.eval v) (ps i)) : Function.Surjective fun (v : ι → R) (i : ι) => (MvPolynomial.eval v) (ps i)

Any injective polynomial map over an algebraic extension of a finite field is surjective.