norm_smul — Mathlib

English

The unit circle acts without changing norms: ‖u • v‖ = ‖v‖ for u ∈ Circle and v in a seminormed space E.

Русский

Единичная окружность сохраняет норму под действием: ‖u • v‖ = ‖v‖, где u ∈ Circle, v ∈ E.

LaTeX

$$$$ \\|u \\cdot v\\| = \\|v\\|, \\quad u \\in \\mathrm{Circle}, v \\in E. $$$$

Lean4

@[simp]
protected theorem norm_smul {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (u : Circle) (v : E) :
    ‖u • v‖ = ‖v‖ := by rw [Submonoid.smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]

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