norm_p_pow

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

For natural n, the norm of p^n equals p^{−n} in the same fashion as zpow behavior.

Русский

Для натурального n норма p^n равна p^{−n}, аналогично поведению zpow.

LaTeX

$$$\|p^{n}\| = p^{-n}$$$

Lean4

@[simp high] -- Shortcut lemma with higher priority.

theorem norm_p_pow (n : ℕ) : ‖(p : ℚ_[p]) ^ n‖ = (p : ℝ) ^ (-n : ℤ) := by rw [← norm_p_zpow, zpow_natCast]

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

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

Разделы

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

Аффилиация

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