Mathlib Map

Theorems · Theorem · logic and foundations

FirstOrder.Field.modelField_of_modelACF

∀ (p : ℕ) (K : Type u_2) [inst : FirstOrder.Language.ring.Structure K] [h : K ⊨ FirstOrder.Language.Theory.ACF p],
  K ⊨ FirstOrder.Language.Theory.field
Defined in
Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
Cited by
3 results in Mathlib
Foundations
Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FirstOrder.Language.StructureFirstOrder.Language.Theory.Model
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FirstOrder.Field.ACF_isComplete · cited by 3Field.ACF_isCompleteFirstOrder.Field.fieldOfModelACF · cited by 3Field.fieldOfModelACFFirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize · cited by 2Field.finite_ACF_prime_no…FirstOrder.Field.ACF_categorical · cited by 1Field.ACF_categoricalSet.ofPred · cited by 6101Set.ofPredSet.image · cited by 5609Set.imageFirstOrder.Language.Structure · cited by 775Language.StructureSet.subset_union_left · cited by 142Set.subset_union_leftFirstOrder.Language.Theory.Model · cited by 67Theory.ModelFirstOrder.Language.ring · cited by 36Language.ringFirstOrder.Language.Theory.ACF · cited by 11Theory.ACFFirstOrder.Language.Theory.field · cited by 6Theory.fieldFirstOrder.Language.Theory.Model.mono · cited by 5Model.monoFirstOrder.Field.genericMonicPolyHasRoot · cited by 4Field.genericMonicPolyHas…Set.subset_union_of_subset_left · cited by 2Set.subset_union_of_subse…Field.modelField_of_modelACFCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.