opNorm_mul_apply — Mathlib

English

Multiplication by an element in a regular normed algebra is an isometry on the underlying normed space.

Русский

Умножение на элемент в регулярном нормированном алгебраическом контексте является изометрией на базовом нормированном пространстве.

LaTeX

$$$\\text{isometry\_mul'}:\\; isometry(\\mathrm{mul}'\\; x)$$$$

Lean4

@[simp]
theorem opNorm_mul_apply (x : R) : ‖mul 𝕜 R x‖ = ‖x‖ :=
  (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 R)).mp (isometry_mul 𝕜 R) x

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