FinitePlace — Mathlib

English

A finite place is associated to an embedding into a completion.

Русский

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

LaTeX

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

Lean4

/-- A finite place of a number field `K` is a place associated to an embedding into a completion
with respect to a maximal ideal. -/
def FinitePlace (K : Type*) [Field K] [NumberField K] :=
  { w : AbsoluteValue K ℝ // ∃ v : HeightOneSpectrum (𝓞 K), place (FinitePlace.embedding v) = w }

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