English
The product of two monoid homomorphisms f and g is a monoid homomorphism defined pointwise by (f·g)(x) = f(x) g(x).
Русский
Произведение двух моноид-гомоморфизмов f и g образует моноид-гомоморфизм: (f·g)(x) = f(x) g(x).
LaTeX
$$$\text{MonoidHom.mul}: (M \to^* N) \times (M \to^* N) \to (M \to^* N)$ с $(f,g)(x) = f(x)\,g(x)$$$
Lean4
/-- Given two monoid morphisms `f`, `g` to a commutative monoid, `f * g` is the monoid morphism
sending `x` to `f x * g x`. -/
@[to_additive]
instance mul : Mul (M →* N) :=
⟨fun f g =>
{ toFun := fun m => f m * g m, map_one' := by simp,
map_mul' := fun x y => by rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)] }⟩
