norm_values_discrete

Mathlib.NumberTheory.Padics.PadicNumbers

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

← MathLib Explorer

English

If a is nonzero, then there exists z such that a.norm = p^{ - z }.

Русский

Если a ≠ 0, то существует z так, что a.norm = p^{ - z }.

LaTeX

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

Lean4

theorem norm_values_discrete (a : PadicSeq p) (ha : ¬a ≈ 0) : ∃ z : ℤ, a.norm = (p : ℚ) ^ (-z) :=
  by
  let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha
  simpa [hk] using padicNorm.values_discrete hk'

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

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

Разделы

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

Аффилиация

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