padic_eq_padicNorm

Mathlib.NumberTheory.Ostrowski

URI: https://scilib.ai/kg/mathlib#Rat.AbsoluteValue.padic_eq_padicNorm

English

For any prime p and rational r, padic(p)(r) equals padicNorm(p)(r).

Русский

Для любого p и рациона r, padic(p)(r) равно padicNorm(p)(r).

LaTeX

$$padic(p)(r) = padicNorm(p)(r)$$

Lean4

@[simp]
theorem padic_eq_padicNorm (p : ℕ) [Fact p.Prime] (r : ℚ) : padic p r = padicNorm p r :=
  rfl

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

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

Разделы

Аффилиация

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