instMulZeroOneClass — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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