instNormOneClass

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The p-adic integers form a NormedDomain, i.e., they form a domain (no zero divisors) equipped with a compatible norm.

Русский

У p-адических целых Z_p есть структура домена с совместной нормой (без делителей нуля).

LaTeX

$$$$\text{IsDomain}(\mathbb{Z}_p).$$$$

Lean4

instance : NormOneClass ℤ_[p] :=
  ⟨norm_def.trans norm_one⟩

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

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

Разделы

Аффилиация

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