instCommCStarAlgebraForall

Mathlib.Analysis.CStarAlgebra.Classes

URI: https://scilib.ai/kg/mathlib#instCommCStarAlgebraForall

English

If each A i is a CommCStarAlgebra, then the product ∏ i A_i is a CommCStarAlgebra.

Русский

Если каждая A_i является коммутативной C*-алгеброй, то произведение ∏_i A_i является CommCStarAlgebra.

LaTeX

$$$$ \\prod_{i \\in ι} A_i \\text{ is a } CommC^*\\text{-algebra} $$$$

Lean4

instance [(i : ι) → CommCStarAlgebra (A i)] : CommCStarAlgebra (Π i, A i) where

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

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

Разделы

Аффилиация

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