Theorems · Theorem · logic and foundations
FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize
∀ (φ : FirstOrder.Language.ring.Sentence),
FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ → {p | ¬FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}.Finite- Cited by
- 2 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites55
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- Finsetproof · cited by 13,712
- SetLike.coeproof · cited by 8,199
- Fieldproof · cited by 7,404
- Set.ofPredstatement and proof · cited by 6,101
- Set.imageproof · cited by 5,609
- Bot.botproof · cited by 4,720
- Compl.complproof · cited by 2,925
- Nontrivialproof · cited by 2,416
- Nat.Primestatement and proof · cited by 2,059
- Set.Finitestatement · cited by 1,814
Cited by2
Results whose statement or proof uses this declaration.
- FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realizeproof · cited by 2
- FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realizeproof · cited by 0