# 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]
[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.