norm_eq_zpow_log_mulValuation

Mathlib.NumberTheory.Padics.PadicNumbers

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

English

The p-adic norm of a nonzero x is given by the exponential of the negative valuation, i.e., ||x|| = exp(-v_p(x)).

Русский

Падиковаeя норма ненулевого x равна exp(−v_p(x)).

LaTeX

$$||x|| = exp(-v_p(x))$$

Lean4

theorem norm_eq_zpow_log_mulValuation {x : ℚ_[p]} (hx : x ≠ 0) : ‖x‖ = (p : ℝ) ^ (log (mulValuation x)) := by
  simp [norm_eq_zpow_neg_valuation, hx]

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

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

Разделы

Аффилиация

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