instNorm

Mathlib.NumberTheory.Padics.PadicNumbers

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

English

The norm on the p-adic numbers is given by padicNormE: ‖x‖ = padicNormE(x).

Русский

Норма на p-адических числах задаётся через padicNormE: ∥x∥ = padicNormE(x).

LaTeX

$$$\|x\| = \mathrm{padicNormE}(x)$$$

Lean4

instance : Norm ℚ_[p] :=
  ⟨fun x ↦ padicNormE x⟩

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

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

Разделы

Аффилиация

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