instCStarAlgebraForall

Mathlib.Analysis.CStarAlgebra.Classes

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

English

If each A i is a C*-algebra for i ∈ ι, then the product ∏ i A i is a C*-algebra.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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