English
Under the same hypotheses as above, there exists a monoid hom smulMonoidHom: α × β →* β defined by (a, b) ↦ a · b, with the property that it sends the unit (1, 1) to 1 in β. This extends the scalar action into a monoid homomorphism.
Русский
При тех же предположениях существует моноид-гомоморфизм smulMonoidHom: α × β →* β, заданный (a, b) ↦ a · b, который отображает единицу на единицу в β. Это расширяет скалярное действие до моноид-гомоморфизма.
LaTeX
$$$\text{smulMonoidHom}: (\alpha \times \beta) \to_* \beta, \; \text{toFun}(a,b) = a \cdot b, \; \text{map_one}' := \text{one_smul } _ _. $$$
Lean4
/-- Scalar multiplication as a monoid homomorphism. -/
@[simps]
def smulMonoidHom [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] : α × β →* β :=
{ smulMulHom with map_one' := one_smul _ _ }
