ACF_isComplete — Mathlib

English

ACF 0 (characteristic zero) is a complete theory.

Русский

ACF 0 (характеристика ноль) является полной теорией.

LaTeX

$$theorem ACF_isComplete {p : Nat} (hp : p.Prime ∨ p = 0) : (Theory.ACF p).IsComplete$$

Lean4

theorem ACF_isComplete {p : ℕ} (hp : p.Prime ∨ p = 0) : (Theory.ACF p).IsComplete :=
  by
  apply Categorical.isComplete.{0, 0, 0} (Order.succ ℵ₀) _ (ACF_categorical _ (Order.lt_succ _)) (Order.le_succ ℵ₀)
  · simp only [card_ring, lift_id']
    exact le_trans (le_of_lt (lt_aleph0_of_finite _)) (Order.le_succ _)
  · exact ACF_isSatisfiable hp
  · rintro ⟨M⟩
    let _ := fieldOfModelACF p M
    have := modelField_of_modelACF p M
    let _ := compatibleRingOfModelField M
    have := isAlgClosed_of_model_ACF p M
    infer_instance

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