starMul — Mathlib

English

If β is a Mul with ContinuousMul and StarMul and ContinuousStar, then C(α, β) is a StarMul, with star applied pointwise: (f g)^* = f^* g^*.

Русский

Если β имеет умножение и сопряжение, то C(α, β) — звездное множество, где star от произведения равен произведению звезд: (f g)^* = f^* g^*.

LaTeX

$$$\mathrm{StarMul}\bigl(C(\alpha, \beta)\bigr)$, with $ (f\cdot g)^*=f^*\cdot g^* $$$

Lean4

instance starMul [Mul β] [ContinuousMul β] [StarMul β] [ContinuousStar β] : StarMul C(α, β) where
  star_mul _ _ := ext fun _ => star_mul _ _

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