toNNReal_valued_eq_adicAbv

Mathlib.NumberTheory.NumberField.FinitePlaces

URI: https://scilib.ai/kg/mathlib#NumberField.toNNReal_valued_eq_adicAbv

English

A finite place is realized by some embedding into a completion.

Русский

Конечное место реализуется вложением в завершение.

LaTeX

$$$\text{FinitePlace}(K) := { w : \mathbb{A}_K \;|\; \exists v,\ \text{place}(\text{embedding } v)=w }$$$

Lean4

theorem toNNReal_valued_eq_adicAbv (x : WithVal (v.valuation K)) :
    toNNReal (absNorm_ne_zero v) (Valued.v x) = adicAbv v x :=
  rfl

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

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

Разделы

Аффилиация

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