norm_eq_norm — Mathlib

English

For any element x in K, the mixedEmbedding norm equals the absolute value of the field norm of x from ℚ to K.

Русский

Для любого элемента x ∈ K, норма смешаннойEmbedding равна модулю абсолютной нормы поля N_{ℚ}^{K}(x).

LaTeX

$$$ \|x\| = |\operatorname{Algebra.norm}_{\mathbb{Q}}(x)| $$$

Lean4

@[simp]
theorem norm_eq_norm (x : K) : mixedEmbedding.norm (mixedEmbedding K x) = |Algebra.norm ℚ x| := by
  simp_rw [mixedEmbedding.norm_apply, normAtPlace_apply, prod_eq_abs_norm]

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