neg

Mathlib.NumberTheory.Padics.PadicNorm

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

← MathLib Explorer

English

The p-adic norm is symmetric in its argument: padicNorm p (−q) = padicNorm p q for all q.

Русский

p-адическая норма симметрична по знаку: padicNorm p (−q) = padicNorm p q.

LaTeX

$$$ padicNorm\ p\ (-q) = padicNorm\ p\ q $$$

Lean4

/-- `padicNorm p` is symmetric. -/
@[simp]
protected theorem neg (q : ℚ) : padicNorm p (-q) = padicNorm p q :=
  if hq : q = 0 then by simp [hq] else by simp [padicNorm, hq]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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