adicAbv_intCast_le_one

Mathlib.NumberTheory.NumberField.FinitePlaces

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

← MathLib Explorer

English

A refined equality relating expMapBasis to sum expansions over fundSystem.

Русский

Уточнение равенства, связывающего expMapBasis с суммированием по fundSystem.

LaTeX

$$$\text{ExpMapBasisApply'}(x) = \dots$$$

Lean4

/-- The `v`-adic absolute value of an integer is `≤ 1`. -/
theorem adicAbv_intCast_le_one (n : ℤ) : adicAbv v n ≤ 1 :=
  (isNonarchimedean_adicAbv v).apply_intCast_le_one_of_isNonarchimedean

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

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

Разделы

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

Аффилиация

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