norm_one

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#PadicSeq.norm_one

English

The norm of the unit element is one: ||1||_p = 1.

Русский

Норма единицы равна единице: ||1||_p = 1.

LaTeX

$$\|1\|_p = 1$$

Lean4

theorem norm_one : norm (1 : PadicSeq p) = 1 :=
  by
  have h1 : ¬(1 : PadicSeq p) ≈ 0 := one_not_equiv_zero _
  simp [h1, norm]

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

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

Разделы

Аффилиация

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