instMonoid — Mathlib

English

The unit sphere is given a Monoid structure (multiplication) inherited from the ambient ring.

Русский

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

LaTeX

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

Lean4

instance instMonoid [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] : Monoid (sphere (0 : 𝕜) 1) :=
  SubmonoidClass.toMonoid (Submonoid.unitSphere 𝕜)

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