norm_def — Mathlib

English

For every p-adic prime p and every p-adic integer z, the norm of z computed in the p-adic integers equals the norm of z when interpreted as an element of the p-adic rationals. In other words, the p-adic norm on Z_p is the restriction of the p-adic norm from Q_p.

Русский

Для любого простого p и любого p-адического целого z нормa z в Z_p равна норме z, рассматриванного как элемент Q_p. Другими словами, норма над Z_p является ограничением нормы над Q_p.

LaTeX

$$$$\|z\| = \|(z : \mathbb{Q}_p)\|.$$$$

Lean4

theorem norm_def {z : ℤ_[p]} : ‖z‖ = ‖(z : ℚ_[p])‖ :=
  rfl

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