norm_const

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

For any nonzero PadicSeq a, there exists an integer z with a.norm = p^{ - z }.

Русский

Для ненулевой PadicSeq a существует целое z такое, что a.norm = p^{ - z }.

LaTeX

$$∃ z ∈ ℤ, a.norm = p^{ - z }$$

Lean4

theorem norm_const (q : ℚ) : norm (const (padicNorm p) q) = padicNorm p q :=
  by
  obtain rfl | hq := eq_or_ne q 0
  · simp [norm]
  · simp [norm, not_equiv_zero_const_of_nonzero hq]

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

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

Разделы

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

Аффилиация

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