norm

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#PadicSeq.norm

← MathLib Explorer

English

For any prime p, the p-adic valuation of p (as a rational) equals exp(-1).

Русский

Для любого p p-адическая оценка числа p (как рационального) равна exp(-1).

LaTeX

$$v_p(p) = \\exp(-1)$$

Lean4

/-- Since the norm of the entries of a Cauchy sequence is eventually stationary,
we can lift the norm to sequences. -/
def norm (f : PadicSeq p) : ℚ :=
  if hf : f ≈ 0 then 0 else padicNorm p (f (stationaryPoint hf))

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

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

Разделы

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

Аффилиация

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