norm_smul — Mathlib

English

For any real scalar c, the norm of c times x equals |c| to the finrank over ℚ(K) times the norm of x.

Русский

Для любого вещественного скаляра c норма c·x равна |c|^{finrank_{ℚ}K} умноженной на норму x.

LaTeX

$$$ \|c \cdot x\| = |c|^{\operatorname{finrank}_{\mathbb{Q}} K} \cdot \|x\| $$$

Lean4

theorem norm_smul (c : ℝ) (x : mixedSpace K) :
    mixedEmbedding.norm (c • x) = |c| ^ finrank ℚ K * (mixedEmbedding.norm x) := by
  simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib, prod_pow_eq_pow_sum, sum_mult_eq]

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