English
A first-order sentence φ is modeled by algebraically closed fields of characteristic zero iff it is modeled by algebraically closed fields of characteristic p for all but finitely many primes p.
Русский
Для любой фрагментной формулы φ она истинна в полях характера нуль тогда и только тогда, когда истинна для всех, кроме конечного числа, простых p, в полях характера p.
LaTeX
$$$\text{Theory.ACF }0 \models \varphi \iff\; \{p : \text{Nat.Primes} \mid \text{Theory.ACF }p \models \varphi\}^c\text{ конечен}.$$$
Lean4
/-- 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 infinitely many `p`. -/
theorem ACF_zero_realize_iff_infinite_ACF_prime_realize {φ : Language.ring.Sentence} :
Theory.ACF 0 ⊨ᵇ φ ↔ Set.Infinite {p : Nat.Primes | Theory.ACF p ⊨ᵇ φ} :=
by
refine
⟨fun h => Set.infinite_of_finite_compl (finite_ACF_prime_not_realize_of_ACF_zero_realize φ h), not_imp_not.1 ?_⟩
simpa [(ACF_isComplete (Or.inr rfl)).models_not_iff,
fun p : Nat.Primes => (ACF_isComplete (Or.inl p.2)).models_not_iff] using
finite_ACF_prime_not_realize_of_ACF_zero_realize φ.not
