adicAbv_natCast_le_one

Mathlib.NumberTheory.NumberField.FinitePlaces

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one

← MathLib Explorer

English

The norm of expMapBasis(x) equals exp(x(w0)) raised to finrank(K/Q).

Русский

Норма expMapBasis(x) равна exp(x(w0))^{finrank(K/ℚ)}.

LaTeX

$$$\text{norm}(\text{expMapBasis}(x)) = \exp(x(w_0))^{\operatorname{finrank}_{\mathbb{Q}} K}$$$

Lean4

/-- The `v`-adic absolute value of a natural number is `≤ 1`. -/
theorem adicAbv_natCast_le_one (n : ℕ) : adicAbv v n ≤ 1 :=
  (isNonarchimedean_adicAbv v).apply_natCast_le_one_of_isNonarchimedean

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

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

Разделы

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

Аффилиация

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