normedField

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

Padic p is a normed field: the p-adic numbers form a NormedField.

Русский

p-адические числа образуют нормированное поле: Padic p — нормированное поле.

LaTeX

$$Padic.padic denotes a NormedField$$

Lean4

instance normedField : NormedField ℚ_[p] :=
  { Padic.field, Padic.metricSpace p with
    dist_eq := fun _ _ ↦ rfl
    norm_mul := by simp [Norm.norm, map_mul]
    norm := norm }

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

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

Разделы

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

Аффилиация

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