padic_le_one

Mathlib.NumberTheory.Ostrowski

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

English

For any prime p and any integer n, padic(p)(n) ≤ 1.

Русский

Для любого простого p и целого числа n, padic(p)(n) ≤ 1.

LaTeX

$$padic(p)(n) ≤ 1$$

Lean4

theorem padic_le_one (p : ℕ) [Fact p.Prime] (n : ℤ) : padic p n ≤ 1 :=
  by
  simp only [padic_eq_padicNorm]
  exact_mod_cast padicNorm.of_int n

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

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

Разделы

Аффилиация

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