instSemigroupWithZero — Mathlib

English

If M₀ and N₀ are Semigroups with zero, then their product M₀ × N₀ is a SemigroupWithZero, i.e., multiplication is associative and zero is absorbing.

Русский

Если M₀ и N₀ — полугруппы с нулём, то их произведение M₀ × N₀ является SemigroupWithZero: умножение ассоциативно, ноль поглощает.

LaTeX

$$$(0,0)\cdot(m,n) = (0,0) \quad\text{and}\quad (m,n)\cdot(0,0) = (0,0)$$$

Lean4

instance instSemigroupWithZero [SemigroupWithZero M₀] [SemigroupWithZero N₀] : SemigroupWithZero (M₀ × N₀)
    where
  zero_mul := by simp
  mul_zero := by simp

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