instCStarRing — Mathlib

English

If β is a nonunital normed ring and has star structure and CStarRing structure, then C(α, β) inherits a CStarRing structure.

Русский

Если β имеет структуру ненулевого нормированного кольца со звездой и CStarRing, то C(α, β) наследует CStarRing.

LaTeX

$$CStarRing (C(\alpha, \beta))$$

Lean4

instance [NonUnitalNormedRing β] [StarRing β] [CStarRing β] : CStarRing C(α, β) where
  norm_mul_self_le
    f := by
    rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), ContinuousMap.norm_le _ (Real.sqrt_nonneg _)]
    intro x
    rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
    exact ContinuousMap.norm_coe_le_norm (star f * f) x

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