instModelACFOfCharPOfIsAlgClosed — Mathlib

English

If K is a field, has characteristic p, and is algebraically closed, then K is a model of ACF p.

Русский

Если K — поле, характеристика которого равна p, и K является алгебраически замкнутым, то K удовлетворяет ACF p.

LaTeX

$$If [Field K] [CompatibleRing K] {p : Nat} [CharP K p] [IsAlgClosed K], then K ⊨ (Theory.ACF p).Model K.$$

Lean4

instance [Field K] [CompatibleRing K] {p : ℕ} [CharP K p] [IsAlgClosed K] : (Theory.ACF p).Model K :=
  by
  refine Theory.model_union_iff.2 ⟨inferInstance, ?_⟩
  simp only [Theory.model_iff, Set.mem_image, forall_exists_index, and_imp]
  rintro _ n hn0 rfl
  simp only [realize_genericMonicPolyHasRoot]
  rintro ⟨p, _, rfl⟩
  exact IsAlgClosed.exists_root p (ne_of_gt (natDegree_pos_iff_degree_pos.1 hn0))

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