Commit 2024-11-20 10:13 6095b78b

View on Github →

feat(ModelTheory): Ax-Grothendieck (#6468)

Estimated changes

Modified Mathlib/FieldTheory/AxGrothendieck.lean

added theorem FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime

added theorem FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero

added theorem FirstOrder.realize_genericPolyMapSurjOnOfInjOn

added theorem ax_grothendieck_of_definable

added theorem ax_grothendieck_univ

added theorem ax_grothendieck_zeroLocus