extensionValuation_apply_coe

Mathlib.Topology.Algebra.Valued.ValuedField

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

English

On the completion, extensionValuation agrees with v on the embedded K.

Русский

На дополнении extensionValuation совпадает с v на внедренном K.

LaTeX

$$$extensionValuation(x) = v(x) \quad (x \in K \subset \hat{K})$$$

Lean4

@[simp]
theorem extensionValuation_apply_coe (x : K) : Valued.extensionValuation (x : hat K) = v x :=
  extension_extends x

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

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

Разделы

Аффилиация

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