norm_apply — Mathlib

English

The global norm is the product over all places of the local norms raised to their multiplicities.

Русский

Глобальная норма есть произведение локальных норм по всем местам, возведённых в кратности мест.

LaTeX

$$$ \operatorname{norm}(x) = \prod_{w} \big( \operatorname{normAtPlace}(w, x) \big)^{\operatorname{mult}(w)} $$$

Lean4

protected theorem norm_apply (x : mixedSpace K) : mixedEmbedding.norm x = ∏ w, (normAtPlace w x) ^ (mult w) :=
  rfl

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