English
For a commutative semigroup α, the map (a,b) ↦ ab from α × α to α is a monoid homomorphism.
Русский
Для коммутативного полугруппы α отображение (a,b) ↦ ab из α × α в α является моноид-гомоморфизмом.
LaTeX
$$$\\text{mulMulHom}: \\alpha \\times \\alpha \\to^* \\alpha\\quad (a,b) \\mapsto ab,\\quad \\text{and } \\text{mulMulHom}((a_1,b_1) \\cdot (a_2,b_2)) = \\text{mulMulHom}(a_1,b_1) \\cdot \\text{mulMulHom}(a_2,b_2).$$$
Lean4
/-- Multiplication as a multiplicative homomorphism. -/
@[to_additive (attr := simps) /-- Addition as an additive homomorphism. -/
]
def mulMulHom [CommSemigroup α] : α × α →ₙ* α where
toFun a := a.1 * a.2
map_mul' _ _ := mul_mul_mul_comm _ _ _ _
