isometry_mul_flip

Mathlib.Analysis.CStarAlgebra.Unitization

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.isometry_mul_flip

English

The flip map of multiplication is an isometry for the norm, i.e., ∥mul flip a∥ = ∥a∥.

Русский

Флип-мэп умножения является изометрией по норме: ∥mul flip a∥ = ∥a∥.

LaTeX

$$$\| (\mathrm{mul}\, \mathit{flip}\, a) \| = \|a\|$$$

Lean4

theorem isometry_mul_flip : Isometry (mul 𝕜 E).flip :=
  AddMonoidHomClass.isometry_of_norm _ (opNorm_mul_flip_apply 𝕜)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru