isAlgebraic — Mathlib

English

PadicAlgCl p is an algebraic extension of ℚ_p, i.e., every element of PadicAlgCl p is a root of a polynomial with coefficients in ℚ_p.

Русский

PadicAlgCl p является алгебраическим расширением ℚ_p; каждый элемент PadicAlgCl p является корнем многочлена с коэффициентами в ℚ_p.

LaTeX

$$$$\mathbb{Q}_p\subseteq \operatorname{PadicAlgCl}(p)\quad\text{is algebraic}.$$$$

Lean4

/-- `PadicAlgCl p` is an algebraic extension of `ℚ_[p]`. -/
theorem isAlgebraic : Algebra.IsAlgebraic ℚ_[p] (PadicAlgCl p) :=
  AlgebraicClosure.isAlgebraic _

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