smulMonoidWithZeroHom — Mathlib

English

Scalar multiplication induces a monoid-with-zero hom from the product M₀ × N₀ to N₀, sending (m, n) to m • n, and preserving zero.

Русский

Кратное умножение порождает гомоморфизм моноида с нулём из произведения M₀ × N₀ в N₀, заданный отображением (m, n) ↦ m • n, сохраняющий нулевой элемент.

LaTeX

$$$\\smulMonoidWithZeroHom : (M_0 \\times N_0) \\to_*_0 N_0,\\quad (m,n) \\mapsto m\\cdot n,\\; \\text{map_zero}' = \\smul_zero _$$

Lean4

/-- Scalar multiplication as a monoid homomorphism with zero. -/
@[simps]
def smulMonoidWithZeroHom [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActionWithZero M₀ N₀] [IsScalarTower M₀ N₀ N₀]
    [SMulCommClass M₀ N₀ N₀] : M₀ × N₀ →*₀ N₀ :=
  { smulMonoidHom with map_zero' := smul_zero _ }

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