English
Let α be a monoid, β a monoid, α acts on β, and the actions commute suitably (IsScalarTower α β β and SMulCommClass α β β). The map smulMulHom: α × β →* β defined by (a, b) ↦ a · b is a monoid homomorphism, i.e., it preserves multiplication: smulMulHom((a1,b1)(a2,b2)) = smulMulHom(a1,b1) smulMulHom(a2,b2).
Русский
Пусть α — моноид, β — моноид, α действует на β, и действия совместимы через соответствующие условия (IsScalarTower α β β и SMulCommClass α β β). Отображение smulMulHom: α × β →* β, задаваемое (a, b) ↦ a · b, является моидомоморфизмом, то есть сохраняет умножение: smulMulHom((a1,b1)(a2,b2)) = smulMulHom(a1,b1) smulMulHom(a2,b2).
LaTeX
$$$\text{smulMulHom}: (\alpha \times \beta) \to_* \beta$, \n \text{toFun}(a,b) = a \cdot b, \n \text{map_mul}'(a_1,b_1,a_2,b_2): (a_1a_2) \cdot (b_1b_2) = (a_1 \cdot b_1)(a_2 \cdot b_2).$$$
Lean4
/-- Scalar multiplication as a multiplicative homomorphism. -/
@[simps]
def smulMulHom [Monoid α] [Mul β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] : α × β →ₙ* β
where
toFun a := a.1 • a.2
map_mul' _ _ := (smul_mul_smul_comm _ _ _ _).symm
