instNormedCommRing — Mathlib

English

The p-adic integers Z_p carry a norm making them a Normed Commutative Ring, with the metric induced by the norm matching the usual distance in the ring.

Русский

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

LaTeX

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

Lean4

instance : NormedCommRing ℤ_[p] where
  __ := instCommRing
  dist_eq := fun ⟨_, _⟩ ⟨_, _⟩ ↦ rfl
  norm_mul_le := by simp [norm_def]

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