instMetricSpace

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The p-adic integers carry an ultrametric distance compatible with the ambient norm.

Русский

У п-адических целых есть ультраметрическое расстояние, совместимое с общей нормой.

LaTeX

$$$\exists$ (IsUltrametricDist $(\mathbb{Z}_p))$$

Lean4

instance : MetricSpace ℤ_[p] :=
  Subtype.metricSpace

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

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

Разделы

Аффилиация

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