instCommMonoid — Mathlib

English

If the ambient ring is a normed commutative ring, the closed unit ball forms a commutative monoid under multiplication.

Русский

Если кольцо — нормированное коммутативное кольцо, то замкнутый единичный шар образует коммутативный моноид по умножению.

LaTeX

$$$\text{If } 𝕜 \text{ is a seminormed commutative ring with norm one, then } \overline{B}(0,1) \text{ is a commutative monoid under multiplication.}$$$

Lean4

instance instCommMonoid [SeminormedCommRing 𝕜] [NormOneClass 𝕜] : CommMonoid (closedBall (0 : 𝕜) 1) :=
  SubmonoidClass.toCommMonoid (Submonoid.unitClosedBall 𝕜)

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