instMulZeroClass — Mathlib

English

If M₀ and N₀ are MulZeroClasses, then their Cartesian product M₀ × N₀ is a MulZeroClass, i.e., zero multiplies to zero on both sides.

Русский

Если M₀ и N₀ обладают структурой MulZeroClass, то их декартово произведение M₀ × N₀ имеет MulZeroClass: ноль умножает слева и справа к нулю.

LaTeX

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

Lean4

instance instMulZeroClass [MulZeroClass M₀] [MulZeroClass N₀] : MulZeroClass (M₀ × N₀)
    where
  zero_mul := by simp [Prod.mul_def]
  mul_zero := by simp [Prod.mul_def]

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