Theorem FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize

Modification history

2024-09-04 10:38
Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
feat(ModelTheory): Lefschetz principle for AlgClosed Fields (#6617) …
Added FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realizeView on Github →