mulMonoidWithZeroHom — Mathlib

English

The map (a,b) ↦ a b is a MonoidWithZeroHom from M × M to M when M is a CommMonoidWithZero.

Русский

Отображение (a,b) ↦ a b является MonoidWithZeroHom: M×M → M, если M — CommMonoidWithZero.

LaTeX

$$$\text{mulMonoidWithZeroHom} : (M \times M) \to^*_0 M\, ,\quad (a,b) \mapsto ab$$$

Lean4

/-- Multiplication as a multiplicative homomorphism with zero. -/
@[simps]
def mulMonoidWithZeroHom [CommMonoidWithZero M₀] : M₀ × M₀ →*₀ M₀
    where
  __ := mulMonoidHom
  map_zero' := mul_zero _

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