padicNorm

Mathlib.NumberTheory.Padics.PadicNorm

URI: https://scilib.ai/kg/mathlib#padicNorm

← MathLib Explorer

English

The element p is a nonunit in ℤ_p.

Русский

Элемент p в ℤ_p не является единицей.

LaTeX

$$p ∈ nonunits(ℤ_[p]).$$

Lean4

/-- If `q ≠ 0`, the `p`-adic norm of a rational `q` is `p ^ (-padicValRat p q)`.
If `q = 0`, the `p`-adic norm of `q` is `0`. -/
def padicNorm (p : ℕ) (q : ℚ) : ℚ :=
  if q = 0 then 0 else (p : ℚ) ^ (-padicValRat p q)

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

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

Разделы

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

Аффилиация

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