English
Let f: R →+* S and g: R →+* T be ring homomorphisms. Then there exists a ring homomorphism f × g: R →+* S × T defined by (f × g)(x) = (f(x), g(x)).
Русский
Пусть f: R →+* S и g: R →+* T — гомоморфизмы колец. Тогда существует кольцевой однородный гомоморфизм f × g: R →+* S × T, заданный формулой (f × g)(x) = (f(x), g(x)).
LaTeX
$$$ (f \\times g) : R \\to+* S \\times T , \\quad (f \\times g)(x) = (f(x), g(x)). $$$
Lean4
/-- Combine two ring homomorphisms `f : R →+* S`, `g : R →+* T` into `f.prod g : R →+* S × T`
given by `(f.prod g) x = (f x, g x)` -/
protected def prod (f : R →+* S) (g : R →+* T) : R →+* S × T :=
{ MonoidHom.prod (f : R →* S) (g : R →* T), AddMonoidHom.prod (f : R →+ S) (g : R →+ T) with
toFun := fun x => (f x, g x) }
