norm_p

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

The norm of the prime element p in the p-adics equals p^{-1}.

Русский

Норма элемента p в p-адических числах равна p^{-1}.

LaTeX

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

Lean4

@[simp]
theorem norm_p : ‖(p : ℚ_[p])‖ = (p : ℝ)⁻¹ :=
  by
  rw [← @Rat.cast_natCast ℝ _ p]
  rw [← @Rat.cast_natCast ℚ_[p] _ p]
  simp [hp.1.ne_zero, norm, padicNorm, padicValRat, padicValInt, zpow_neg, -Rat.cast_natCast]

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

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

Разделы

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

Аффилиация

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