English
Given monoid homomorphisms f: M → N and g: M → P, their product f.prod g is a monoid homomorphism M → N × P defined by x ↦ (f(x), g(x)).
Русский
Пусть f: M → N и g: M → P — моноид-гомоморфизм; их произведение f.prod g является моноид-гомоморфизмом M → N × P, заданным x ↦ (f(x), g(x)).
LaTeX
$$$f: M \to N$, $g: M \to P$ ⇒ $f.prod g: M \to (N \times P)$, $ (f.prod g)(x)=(f(x),g(x))$ and $(f.prod g)(xy)=(f(x)f(y),\,g(x)g(y))$.$$
Lean4
/-- Combine two `MonoidHom`s `f : M →ₙ* N`, `g : M →ₙ* P` into
`f.prod g : M →ₙ* (N × P)` given by `(f.prod g) x = (f x, g x)`. -/
@[to_additive prod /-- Combine two `AddMonoidHom`s `f : AddHom M N`, `g : AddHom M P` into
`f.prod g : AddHom M (N × P)` given by `(f.prod g) x = (f x, g x)` -/
]
protected def prod (f : M →ₙ* N) (g : M →ₙ* P) : M →ₙ* N × P
where
toFun := Pi.prod f g
map_mul' x y := Prod.ext (f.map_mul x y) (g.map_mul x y)
