English
Given ring homomorphisms f: R → S and g: R → T, the map f.prod g: R → S × T sends x to (f(x), g(x)).
Русский
Для гомоморфизмов f:R→S и g:R→T отображение f.prod g: R → S × T отправляет x в (f(x), g(x)).
LaTeX
$$$f: R \\to_{} S,\; g: R \\to_{} T \\Rightarrow\\; f.prod g: R \\to_{} S \\times T, \\; (f.prod g)(x)=(f(x),g(x)).$$$
Lean4
/-- Combine two non-unital 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 :=
{ MulHom.prod (f : MulHom R S) (g : MulHom R T), AddMonoidHom.prod (f : R →+ S) (g : R →+ T) with
toFun := fun x => (f x, g x) }
