Theorems · Theorem · logic and foundations

FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize

∀ {φ : FirstOrder.Language.ring.Sentence},
  FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ ↔ {p | FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}.Infinite

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.

Defined in

Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Cited by

2 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound