English
Let (R_i) be a finite family of C*-rings indexed by i. The product ∏_i R_i is a C*-ring, and the standard norm inequality ∥x x*∥ ≤ ∥x∥^2 holds componentwise.
Русский
Пусть (R_i) – конечная семья C*-колец индексируемая i. Произведение ∏_i R_i является C*-кольцом, справедливо неравенство нормы ∥x x*∥ ≤ ∥x∥^2 по компонентам.
LaTeX
$$$ \|x x^{\star}\| \leq \|x\|^2 $$$
Lean4
instance _root_.Pi.cstarRing : CStarRing (∀ i, R i) where
norm_mul_self_le
x := by
refine le_of_eq (Eq.symm ?_)
simp only [norm, Pi.mul_apply, Pi.star_apply, nnnorm_star_mul_self, ← sq]
norm_cast
exact
(Finset.comp_sup_eq_sup_comp_of_is_total (fun x : NNReal => x ^ 2)
(fun x y h => by simpa only [sq] using mul_le_mul' h h) (by simp)).symm
