English
The theory of algebraically closed fields of characteristic p, considered in the language of rings, is the union of the theory of fields of characteristic p and the set of sentences asserting that all monic polynomials have roots for positive degrees.
Русский
Теория алгебраически замкнутых полей характера p, рассматриваемая в языке колец, является объединением теории полей с характеристикой p и множества утверждений о существовании корней у всех мономных многочленов положной степени.
LaTeX
$$$\mathrm{ACF}(p) = \mathrm{Theory.fieldOfChar}(p) \cup \mathrm{genericMonicPolyHasRoot}'' \{n \mid 0 < n\}$$$
Lean4
/-- The theory of algebraically closed fields of characteristic `p` as a theory over
the language of rings -/
def _root_.FirstOrder.Language.Theory.ACF (p : ℕ) : Theory .ring :=
Theory.fieldOfChar p ∪ genericMonicPolyHasRoot '' {n | 0 < n}
