integers — Mathlib

English

For a prime p, the valuation ring 𝓞_ℂ_[p] is the ring of integers of the valued field PadicComplex p.

Русский

Для простого p кольцо валюаций 𝓞_ℂ_[p] является кольцом целых валюированного поля PadicComplex p.

LaTeX

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

Lean4

/-- `𝓞_ℂ_[p]` is the ring of integers of `ℂ_[p]`. -/
theorem integers : Valuation.Integers (PadicComplex.valued p).v 𝓞_ℂ_[p] :=
  Valuation.integer.integers _

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