norm_int_le_one

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#Padic.norm_int_le_one

English

If z ∈ ℤ, then the p-adic norm of z is at most 1.

Русский

Если z ∈ ℤ, то p-адическая норма z не превосходит 1.

LaTeX

$$$\\forall z\\in\\mathbb{Z},\\ \\|z\\|_p \\le 1$$$

Lean4

theorem norm_int_le_one (z : ℤ) : ‖(z : ℚ_[p])‖ ≤ 1 :=
  suffices ‖((z : ℚ) : ℚ_[p])‖ ≤ 1 by simpa
  norm_rat_le_one <| by simp [hp.1.ne_one]

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

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

Разделы

Аффилиация

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