opNNNorm_mul_apply — Mathlib

English

The operator norm of the multiplication map equals the value of the norm of the input, in many standard contexts.

Русский

Операторная норма отображения умножения равна норме входного элемента в большинстве стандартных контекстов.

LaTeX

$$$\|mul\;x\|_{op} = \|x\|$$$

Lean4

@[simp]
theorem opNNNorm_mul_apply (x : R) : ‖mul 𝕜 R x‖₊ = ‖x‖₊ :=
  Subtype.ext <| opNorm_mul_apply 𝕜 R x

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