cstarRing — Mathlib

English

If R1 and R2 are C*-rings, then their product R1 × R2 carries a C*-ring structure; in particular, the norm satisfies ∥x x*∥ ≤ ∥x∥^2 for any x in the product.

Русский

Если R1 и R2 – C*-кольца, то их произведение R1 × R2 имеет структуру C*-кольца; в частности, норма удовлетворяет ∥x x*∥ ≤ ∥x∥^2 для любого x в произведении.

LaTeX

$$$ \|x x^{\star}\| \leq \|x\|^2 $$$

Lean4

instance _root_.Prod.cstarRing : CStarRing (R₁ × R₂) where
  norm_mul_self_le
    x := by
    dsimp only [norm]
    simp only [Prod.fst_mul, Prod.fst_star, Prod.snd_mul, Prod.snd_star, norm_star_mul_self, ← sq]
    rw [le_sup_iff]
    rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h) <;> simp [h]

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