instMulOpposite — Mathlib

English

For a nonunital normed ring E with a star operation, the opposite ring Eᵐᵒᵖ inherits a C*-ring structure with the same norm-inequality norm_mul_self_le, applied to unop.

Русский

Для неабстрактного нормированного кольца E с операцией звезды, противоположное кольцо Eᵐᵒᵖ наследует структуру C*-кольца; неравенство norm_mul_self_le применяется к unop.

LaTeX

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

Lean4

instance {E : Type*} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] : CStarRing Eᵐᵒᵖ where
  norm_mul_self_le x := CStarRing.norm_self_mul_star (x := MulOpposite.unop x) |>.symm.le

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