English
If two elements x and y have identical norms at every place, then their global norms are equal.
Русский
Если для всех мест нормы нормAtPlace совпадают для x и y, то их глобальные нормы равны.
LaTeX
$$$ (\forall w, \operatorname{normAtPlace}(w, x) = \operatorname{normAtPlace}(w, y)) \;\Rightarrow\; \operatorname{norm}(x) = \operatorname{norm}(y) $$$
Lean4
/-- The norm of `x` is `∏ w, (normAtPlace x) ^ mult w`. It is defined such that the norm of
`mixedEmbedding K a` for `a : K` is equal to the absolute value of the norm of `a` over `ℚ`,
see `norm_eq_norm`. -/
protected def norm : (mixedSpace K) →*₀ ℝ
where
toFun x := ∏ w, (normAtPlace w x) ^ (mult w)
map_one' := by simp only [map_one, one_pow, prod_const_one]
map_zero' := by simp [mult]
map_mul' _ _ := by simp only [map_mul, mul_pow, prod_mul_distrib]
