isAlgClosed_of_model_ACF — Mathlib

English

If K is a model of ACF p, then K is algebraically closed.

Русский

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

LaTeX

$$theorem isAlgClosed_of_model_ACF (p : Nat) (K : Type*) [Field K] [CompatibleRing K] [h : (Theory.ACF p).Model K] : IsAlgClosed K$$

Lean4

theorem isAlgClosed_of_model_ACF (p : ℕ) (K : Type*) [Field K] [CompatibleRing K] [h : (Theory.ACF p).Model K] :
    IsAlgClosed K := by
  refine IsAlgClosed.of_exists_root _ ?_
  intro p hpm hpi
  have h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n} := Theory.Model.mono h (by simp [Theory.ACF])
  simp only [Theory.model_iff, Set.mem_image, forall_exists_index, and_imp] at h
  have := h _ p.natDegree (natDegree_pos_iff_degree_pos.2 (degree_pos_of_irreducible hpi)) rfl
  rw [realize_genericMonicPolyHasRoot] at this
  exact this ⟨_, hpm, rfl⟩

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