valuedCompletion_apply

Mathlib.Topology.Algebra.Valued.ValuedField

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

English

On the base field K, the valued completion valuation coincides with v.

Русский

На поле K валюационная оценка в дополнении совпадает с v.

LaTeX

$$$Valued.v (x : hat{K}) = v x$$$

Lean4

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

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

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

Разделы

Аффилиация

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