Completion

Mathlib.NumberTheory.NumberField.InfinitePlace.Completion

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.Completion

English

For x in WithAbs v.1, the norm of its image in the completion equals v applied to the corresponding element.

Русский

Для x в WithAbs v.1 норма образа в дополнении равна применению v к соответствующему элементу.

LaTeX

$$$\|(x : v.\!Completion)\| = v (WithAbs.equiv v.1 x)$$$

Lean4

/-- The completion of a number field at an infinite place. -/
abbrev Completion :=
  v.1.Completion

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

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

Разделы

Аффилиация

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