norm_coe — Mathlib

English

For v a real infinite place, the norm in the completion at v agrees with the usual absolute value on the base field.

Русский

Для вещественного бесконечного места норма в дополнении согласуется с обычной абсолютной величиной на базовом поле.

LaTeX

$$$\|x\| = |x|$ in completion for Rat$$

Lean4

theorem norm_coe (x : WithAbs v.1) : ‖(x : v.Completion)‖ = v (WithAbs.equiv v.1 x) :=
  UniformSpace.Completion.norm_coe x

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