norm_smulRight — Mathlib

English

In the empty-index setting, the norm of the constant map equals the norm of the input, establishing a simple baseline for norms of constant multilinear maps on empty index sets.

Русский

В пустом индексе норма константного отображения равна норме входного вектора.

LaTeX

$$$\|\mathrm{constOfIsEmpty}_{\mathbb{K}}(E,x)\| = \|x\|$$$

Lean4

@[simp]
theorem norm_smulRight (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) : ‖f.smulRight z‖ = ‖f‖ * ‖z‖ :=
  congr_arg NNReal.toReal (nnnorm_smulRight f z)

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