PadicInt

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt

English

ℤ_p is the p-adic integers; there is an isometric embedding ℤ_p → ℚ_p via the inclusion map.

Русский

ℤ_p встраивается из п-адических целых в ℚ_p без искажения дистанции.

LaTeX

$$$$ \\mathbb{Z}_p \\hookrightarrow \\mathbb{Q}_p, \\; x \\mapsto x. $$$$

Lean4

/-- The `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. -/
def PadicInt : Type :=
  { x : ℚ_[p] // ‖x‖ ≤ 1 }

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru