English
For p prime or p = 0, there exists an algebraically closed field of characteristic p, so the theory ACF p is satisfiable.
Русский
Для простого p или p = 0 существует алгебраически замкнутое поле характеристики p, следовательно теория ACF p удовлетворима.
LaTeX
$$theorem ACF_isSatisfiable {p : Nat} (hp : p.Prime ∨ p = 0) : (Theory.ACF p).IsSatisfiable$$
Lean4
theorem ACF_isSatisfiable {p : ℕ} (hp : p.Prime ∨ p = 0) : (Theory.ACF p).IsSatisfiable := by
cases hp with
| inl hp =>
have : Fact p.Prime := ⟨hp⟩
let _ := compatibleRingOfRing (AlgebraicClosure (ZMod p))
have : CharP (AlgebraicClosure (ZMod p)) p :=
charP_of_injective_algebraMap (RingHom.injective (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) p
exact ⟨⟨AlgebraicClosure (ZMod p)⟩⟩
| inr hp =>
subst hp
let _ := compatibleRingOfRing (AlgebraicClosure ℚ)
have : CharP (AlgebraicClosure ℚ) 0 :=
charP_of_injective_algebraMap (RingHom.injective (algebraMap ℚ (AlgebraicClosure ℚ))) 0
exact ⟨⟨AlgebraicClosure ℚ⟩⟩
