extension — Mathlib

English

There exists an extension of the valuation to the completion hat K, i.e., a map extension : hat K → Γ₀ extending v.

Русский

Существуют расщирение валюации на заменение hat K — дополнение, т.е. отображение extension: hat K → Γ₀ расширяющее v.

LaTeX

$$$extension: \hat{K} \to Γ_0$$$

Lean4

/-- The extension of the valuation of a valued field to the completion of the field. -/
noncomputable def extension : hat K → Γ₀ :=
  Completion.isDenseInducing_coe.extend (v : K → Γ₀)

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