one

Mathlib.NumberTheory.Padics.PadicNorm

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

English

PadicNorm of 1 is 1 in any p.

Русский

PadicNorm(1) = 1 для любого p.

LaTeX

$$padicNorm p 1 = 1.$$

Lean4

/-- The `p`-adic norm of `1` is `1`. -/
protected theorem one : padicNorm p 1 = 1 := by simp [padicNorm]

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

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

Разделы

Аффилиация

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