Theorems · Theorem · logic and foundations
FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize
∀ {φ : FirstOrder.Language.ring.Sentence},
FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ ↔ {p | FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}ᶜ.FiniteAnother 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.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.ofPredstatement and proof · cited by 6,101
- Compl.complstatement and proof · cited by 2,925
- Nat.Primestatement · cited by 2,059
- Set.Finitestatement and proof · cited by 1,814
- FirstOrder.Language.Sentencestatement and proof · cited by 127
- Nat.Primesstatement and proof · cited by 63
- FirstOrder.Language.ringstatement and proof · cited by 36
- FirstOrder.Language.Theory.ModelsBoundedFormulastatement and proof · cited by 30
- FirstOrder.Language.Theory.ACFstatement and proof · cited by 11
- Set.infinite_of_finite_complproof · cited by 2
- FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realizeproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.