English
Given f: M →* N and g: M →* P, define their product map f.prod g: M →* N × P by (f.prod g)(x) = (f(x), g(x)).
Русский
Пусть f: M →* N и g: M →* P. Тогда отображение f.prod g: M →* N × P задаётся как (f(x), g(x)).
LaTeX
$$$ (f \\prod g)(x) = (f(x), g(x)). $$$
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 : M →+ N`, `g : M →+ P` into
`f.prod g : 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_one' := Prod.ext f.map_one g.map_one
map_mul' x y := Prod.ext (f.map_mul x y) (g.map_mul x y)
