PadicAlgCl — Mathlib

English

PadicAlgCl(p) is defined as the algebraic closure of ℚ_p, i.e., PadicAlgCl(p) ≅ algebraic closure of ℚ_p.

Русский

PadicAlgCl(p) определяется как алгебраическое замыкание ℚ_p, то есть PadicAlgCl(p) эквивалентно алгебраическому замыканию ℚ_p.

LaTeX

$$$$\operatorname{PadicAlgCl}(p) \cong \operatorname{AlgebraicClosure}(\mathbb{Q}_p).$$$$

Lean4

/-- `PadicAlgCl p` is a fixed algebraic closure of `ℚ_[p]`. -/
abbrev PadicAlgCl :=
  AlgebraicClosure ℚ_[p]

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