instMonoid — Mathlib

English

The closed unit ball is a monoid with zero under multiplication; it has a multiplicative identity and 0 acts as a zero element.

Русский

Замкнутый единичный шар является моноидом с нулём по умножению; у него есть единица умножения, и 0 действует как нулевой элемент.

LaTeX

$$$\forall x,y \in \overline{B}(0,1),\; xy \in \overline{B}(0,1) \land 0 \cdot x = 0 \land x \cdot 0 = 0$$$

Lean4

instance instMonoid [SeminormedRing 𝕜] [NormOneClass 𝕜] : Monoid (closedBall (0 : 𝕜) 1) :=
  SubmonoidClass.toMonoid (Submonoid.unitClosedBall 𝕜)

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