norm_def'

Mathlib.Analysis.CStarAlgebra.Multiplier

URI: https://scilib.ai/kg/mathlib#DoubleCentralizer.norm_def'

English

The norm on 𝓜(𝕜,A) agrees with the norm obtained from its image under theProd homomorphism to the product, i.e., ‖a‖ = ‖toProdHom(a)‖.

Русский

Норма на 𝓜(𝕜,A) совпадает с нормой образа через отображение toProdHom; ‖a‖ = ‖toProdHom(a)‖.

LaTeX

$$$\|a\| = \|\mathrm{toProdHom}(a)\|$$$

Lean4

theorem norm_def' (a : 𝓜(𝕜, A)) : ‖a‖ = ‖toProdMulOppositeHom a‖ :=
  rfl

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

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

Разделы

Аффилиация

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