instMonoidWithZero — Mathlib

English

If M₀ and N₀ are CommMonoidWithZero, then their product M₀ × N₀ is a CommMonoidWithZero.

Русский

Если M₀ и N₀ — коммутативные моноиды с нулём, то их произведение является CommMonoidWithZero.

LaTeX

$$$(0,0) = (0,0) \quad\text{and}\quad (a,b) \cdot (c,d) = (ac, bd)$$$

Lean4

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

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