fieldOfModelACF — Mathlib

English

A model for the ACF p theory yields a field K with a field structure.

Русский

Модель для теории ACF p задаёт поле K с полевой структурой.

LaTeX

$$def fieldOfModelACF (p : Nat) (K : Type*) [ L.ring.Structure K] [h : (Theory.ACF p).Model K] : Field K$$

Lean4

/-- A model for the Theory of algebraically closed fields is a Field. After introducing
this as a local instance on a particular Type, you should usually also introduce
`modelField_of_modelACF p M`, `compatibleRingOfModelField` and `isAlgClosed_of_model_ACF` -/
@[reducible]
noncomputable def fieldOfModelACF (p : ℕ) (K : Type*) [Language.ring.Structure K] [h : (Theory.ACF p).Model K] :
    Field K := by
  have := modelField_of_modelACF p K
  exact fieldOfModelField K

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