padicValInt_self

Mathlib.NumberTheory.Padics.PadicVal.Basic

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

English

The p-adic valuation of p itself equals 1.

Русский

p-адическая оценка самого p равна 1.

LaTeX

$$$\\operatorname{padicValInt} p p = 1$$$

Lean4

theorem padicValInt_self : padicValInt p p = 1 :=
  padicValInt.self hp.out.one_lt

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

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

Разделы

Аффилиация

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