instCStarAlgebraComplex

Mathlib.Analysis.CStarAlgebra.Multiplier

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

English

There is a C*-algebra structure on the complexified multiplier algebra 𝓜(ℂ,A) for any nonunital C*-algebra A.

Русский

Существет структура C*-алгебры на комплексизированной мультипликаторной алгебре 𝓜(ℂ,A).

LaTeX

$$$\mathcal{M}(\mathbb{C},A) \text{ is a } C^*\text{-algebra}$$$

Lean4

noncomputable instance {A : Type*} [NonUnitalCStarAlgebra A] : CStarAlgebra 𝓜(ℂ, A) where

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

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

Разделы

Аффилиация

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