embedding — Mathlib

English

There is a natural embedding from the number field into its v-adic completion via a finite place.

Русский

Существует естественное вложение числа поля в его v-адик завершение через конечное место.

LaTeX

$$$\text{embedding}:\ WithVal(v.valuation\ K) \hookrightarrow \text{adicCompletion}(K,v)$$$

Lean4

/-- The embedding of a number field inside its completion with respect to `v`. -/
noncomputable def embedding : WithVal (v.valuation K) →+* adicCompletion K v :=
  UniformSpace.Completion.coeRingHom

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