instCommMonoidWithZero — Mathlib

English

The direct product M₀ × N₀ of two commutative monoids with zero is a commutative monoid with zero; zero is (0,0) and 0·a = 0, a·0 = 0.

Русский

Детерминированное произведение M₀ × N₀ двух коммутативных моноидов с нулём является коммутативным моноидом с нулём; ноль — это (0,0), и 0·a = 0, a·0 = 0.

LaTeX

$$$((0,0) \cdot (a,b)) = (0,0) \quad\text{and}\quad ((a,b) \cdot (0,0)) = (0,0)$$$

Lean4

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

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