norm_fst

Mathlib.Analysis.CStarAlgebra.Multiplier

URI: https://scilib.ai/kg/mathlib#DoubleCentralizer.norm_fst

← MathLib Explorer

English

The norm of a.fst equals the norm of a itself in the multiplier algebra.

Русский

Норма a.fst равна норме a в 𝓜(𝕜,A).

LaTeX

$$$\|a.fst\| = \|a\|$$$

Lean4

@[simp]
theorem norm_fst (a : 𝓜(𝕜, A)) : ‖a.fst‖ = ‖a‖ := by
  simp only [norm_def, toProdHom_apply, Prod.norm_def, norm_fst_eq_snd, max_eq_right le_rfl]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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