instCommMonoid — Mathlib

English

If the ambient ring is a normed commutative ring, the unit sphere is a CommMonoid under multiplication.

Русский

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

LaTeX

$$$\text{CommMonoid} (S)$ under multiplication$$

Lean4

instance instCommMonoid [SeminormedCommRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : CommMonoid (sphere (0 : 𝕜) 1) :=
  SubmonoidClass.toCommMonoid (Submonoid.unitSphere 𝕜)

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