instSemigroupWithZero — Mathlib

English

The closed unit ball around 0, under multiplication inherited from the ambient ring, forms a semigroup with zero; in particular, 0 acts as a absorbing element.

Русский

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

LaTeX

$$$\overline{B}(0,1) \cdot \overline{B}(0,1) \subseteq \overline{B}(0,1) \quad\land\quad 0 \cdot x = 0 \quad\text{и}\quad x \cdot 0 = 0\text{ для всех }x.$$$

Lean4

instance instSemigroupWithZero [NonUnitalSeminormedRing 𝕜] : SemigroupWithZero (closedBall (0 : 𝕜) 1)
    where
  zero_mul _ := Subtype.eq <| zero_mul _
  mul_zero _ := Subtype.eq <| mul_zero _

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