ax_grothendieck_of_locally_finite

theorem ax_grothendieck_of_locally_finite : ∀ {ι : Type u_1} {K : Type u_2} {R : Type u_3} [inst : Field K] [inst_1 : Finite K] [inst_2 : CommRing R] [inst_3 : Finite ι] [inst_4 : Algebra K R], Algebra.IsAlgebraic K R → ∀ (ps : ι → MvPolynomial ι R), (Function.Injective fun v i => (MvPolynomial.eval v) (ps i)) → Function.Surjective fun v i => (MvPolynomial.eval v) (ps i)

This theorem, named `ax_grothendieck_of_locally_finite`, states that for any type `ι`, any field `K`, any type `R` with a field structure, an algebra structure over `K` and `R`, and any function `ps` from `ι` to multivariate polynomials over `ι` and `R`, if `K` is finite, `ι` is finite, `R` is a commutative ring, and `R` is an algebraic extension of `K`, then any injective polynomial map, defined as the function that takes a valuation `v` and an index `i`, and evaluates the polynomial `ps i` at `v`, is also surjective. In other words, given certain conditions, any value in the codomain of this polynomial map can be obtained by evaluating the map for some input in its domain.

More concisely: If `K` is a finite field, `ι` is finite, `R` is a commutative ring and an algebraic extension of `K`, and `ps` is a function from `ι` to multivariate polynomials over `ι` and `R`, then any injective polynomial map from `ι` to `R` induced by `ps` is surjective.