isNonarchimedean_adicAbv

Mathlib.RingTheory.DedekindDomain.AdicValuation

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv

← MathLib Explorer

English

The v-adic absolute value is nonarchimedean; see above.

Русский

Неархимедово неравенство для адик-абв; как выше.

LaTeX

$$Theorem isNonarchimedean_adicAbv v hb$$

Lean4

/-- The `v`-adic absolute value is nonarchimedean -/
theorem isNonarchimedean_adicAbv (v : HeightOneSpectrum R) {b : NNReal} (hb : 1 < b) :
    IsNonarchimedean (α := K) (v.adicAbv hb) :=
  isNonarchimedean_adicAbvDef v hb

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

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

Разделы

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

Аффилиация

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