Commit 2023-05-23 01:34 bd7d776e

View on Github →

feat: port FieldTheory.AxGrothendieck (#4237)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/AxGrothendieck.lean

added theorem ax_grothendieck_of_locally_finite