PadicComplexInt — Mathlib

English

Let p be a prime. The subring of the p-adic complex field C_p consisting of elements whose valuation is at most 1 is a valuation subring, commonly denoted 𝓞_ℂ_[p].

Русский

Пусть p — простое число. Подкольцо комплексной падиковой области C_p, состоящее из элементов с валюацией ≤ 1, является оцениваемым подкольцом, обозначаемым 𝓞_ℂ_[p].

LaTeX

$$$\\mathcal{O}_{\\mathbb{C}_p} = \\{ x \\in \\mathbb{C}_p : v(x) \\le 1 \\}$$$

Lean4

/-- We define `𝓞_ℂ_[p]` as the valuation subring of `ℂ_[p]`, consisting of those elements with
  valuation `≤ 1`. -/
def PadicComplexInt : ValuationSubring ℂ_[p] :=
  (PadicComplex.valued p).v.valuationSubring

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