modelField_of_modelACF — Mathlib

English

If K satisfies ACF p in the ring-language, then K carries a field-structure modeling the theory of fields.

Русский

Если K удовлетворяет ACF p в языке колец, то K обладает полевой структурой, которая моделирует теорию полей.

LaTeX

$$If [Field K] [CompatibleRing K] {p : Nat} [CharP K p] [IsAlgClosed K], then Theory.field.Model K.$$

Lean4

theorem modelField_of_modelACF (p : ℕ) (K : Type*) [Language.ring.Structure K] [h : (Theory.ACF p).Model K] :
    Theory.field.Model K :=
  Theory.Model.mono h (Set.subset_union_of_subset_left Set.subset_union_left _)

Похожие утверждения