instSemigroupWithZero — Mathlib

English

The ball is a semigroup with zero under multiplication: zero is absorbing, i.e., 0·x = 0 and x·0 = 0 for all x in the ball.

Русский

Шар образует полугруппу с нулём под умножением: нуль поглощает, то есть 0·x = 0 и x·0 = 0 для всех x в шаре.

LaTeX

$$$\\forall x \\in \\text{ball}(0,1),\\; 0\\cdot x = 0 = x\\cdot 0$$$

Lean4

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

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