English
A first-order sentence φ is modeled by algebraically closed fields of characteristic zero iff the set {p prime | ACF p ⊨ φ} has finite complement.
Русский
Для первой‑порядковой формулы φ истинна в теории алгебраически замкнутых полей характера нуль тогда и только тогда, когда множество простых p, для которых ACF p ⊨ φ, имеет конечный комплемента.
LaTeX
$$$\text{Theory.ACF }0 \models φ \iff \mathrm{Fin}(\{p : \mathbb{N}_{\text{prime}} \mid \text{Theory.ACF }p \models φ\}^c).$$$
Lean4
/-- Another statement of the **Lefschetz principle**. A first-order sentence is modeled by the
theory of algebraically closed fields of characteristic zero if and only if it is modeled by the
theory of algebraically closed fields of characteristic `p` for all but finitely many primes `p`.
-/
theorem ACF_zero_realize_iff_finite_ACF_prime_not_realize {φ : Language.ring.Sentence} :
Theory.ACF 0 ⊨ᵇ φ ↔ Set.Finite {p : Nat.Primes | Theory.ACF p ⊨ᵇ φ}ᶜ :=
⟨fun h => finite_ACF_prime_not_realize_of_ACF_zero_realize φ h, fun h =>
ACF_zero_realize_iff_infinite_ACF_prime_realize.2 (Set.infinite_of_finite_compl h)⟩
