norm_neg

Mathlib.NumberTheory.Padics.PadicNumbers

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

English

The norm is invariant under negation: (−a).norm = a.norm.

Русский

Норма не меняется при взятии противоположного: (−a).norm = a.norm.

LaTeX

$$(-a).norm = a.norm$$

Lean4

theorem norm_neg (a : PadicSeq p) : (-a).norm = a.norm :=
  norm_eq <| by simp

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

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

Разделы

Аффилиация

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