norm_eq_zpow_neg_valuation

Mathlib.NumberTheory.Padics.PadicIntegers

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

← MathLib Explorer

English

For nonzero x, the p-adic norm equals p^{−valuation(x)}.

Русский

Для ненулевого x норма p-адических чисел равна p^{−v_p(x)}.

LaTeX

$$\|x\| = p^{-\, x.valuation}$$

Lean4

theorem norm_eq_zpow_neg_valuation {x : ℤ_[p]} (hx : x ≠ 0) : ‖x‖ = p ^ (-x.valuation : ℤ) := by
  simp [norm_def, Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx]
    -- TODO: Do we really need this lemma?

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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