norm_le_one

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

Any element of Z_p has norm at most 1: for all z in Z_p, ||z|| ≤ 1.

Русский

Любой элемент Z_p имеет норму не более 1: для всякого z ∈ Z_p выполнено ||z|| ≤ 1.

LaTeX

$$$$\|z\| \le 1 \quad \text{for all } z \in \mathbb{Z}_p.$$$$

Lean4

theorem norm_le_one (z : ℤ_[p]) : ‖z‖ ≤ 1 :=
  z.2

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

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

Разделы

Аффилиация

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