norm_eq_of_normAtPlace_eq — Mathlib

English

If the local norms agree for all places, the global norms agree.

Русский

Если локальные нормы совпадают для всех мест, совпадают и глобальные нормы.

LaTeX

$$$ (\forall w, \operatorname{normAtPlace}(w, x) = \operatorname{normAtPlace}(w, y)) \Rightarrow \|x\| = \|y\| $$$

Lean4

theorem norm_eq_of_normAtPlace_eq {x y : mixedSpace K} (h : ∀ w, normAtPlace w x = normAtPlace w y) :
    mixedEmbedding.norm x = mixedEmbedding.norm y := by simp_rw [mixedEmbedding.norm_apply, h]

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