instCommSemigroup — Mathlib

English

The unit ball is a commutative semigroup under multiplication when the ambient ring is commutative.

Русский

Единичная сфера образует коммутативную полугруппу под умножением, если окружение коммутативно.

LaTeX

$$$\\forall x,y \\in \\text{ball}(0,1),\\; xy = yx$$$

Lean4

instance instCommSemigroup [SeminormedCommRing 𝕜] : CommSemigroup (ball (0 : 𝕜) 1) :=
  MulMemClass.toCommSemigroup (Subsemigroup.unitBall 𝕜)

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