norm_p_zpow

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

For any integer n, ‖p^n‖_p = p^{−n}.

Русский

Для любого целого n выполняется ‖p^n‖_p = p^{−n}.

LaTeX

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

Lean4

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

theorem norm_p_zpow (n : ℤ) : ‖(p : ℚ_[p]) ^ n‖ = (p : ℝ) ^ (-n) := by rw [norm_zpow, norm_p, zpow_neg, inv_zpow]

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

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

Разделы

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

Аффилиация

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