extension_extends

Mathlib.Topology.Algebra.Valued.ValuedField

URI: https://scilib.ai/kg/mathlib#Valued.extension_extends

← MathLib Explorer

English

For each x in K, extension(x) equals v(x).

Русский

Для каждого x в K, extension(x) = v(x).

LaTeX

$$$extension(x) = v(x) \quad (x \in K \hookrightarrow \hat{K})$$$

Lean4

@[simp, norm_cast]
theorem extension_extends (x : K) : extension (x : hat K) = v x :=
  by
  refine Completion.isDenseInducing_coe.extend_eq_of_tendsto ?_
  rw [← Completion.isDenseInducing_coe.nhds_eq_comap]
  exact Valued.continuous_valuation.continuousAt

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

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

Разделы

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

Аффилиация

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