opNorm_mul — Mathlib

English

The operator norm of the left-multiplication by elements of R on E is 1 in the sense that the operator from R to L(E,E) given by x ↦ (y ↦ x·y) has norm 1.

Русский

Норма оператора слева на умножение на элементы R равна 1 в смысле нормы отображения x ↦ (y ↦ x·y).

LaTeX

$$$\\|\\mathrm{mul}_{\\mathbb{K},R}\\| = 1$$$

Lean4

@[simp]
theorem opNorm_mul : ‖mul 𝕜 R‖ = 1 :=
  (mulₗᵢ 𝕜 R).norm_toContinuousLinearMap

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