feat(algebra/algebra/basic):add alg_hom.prod (#16116)

This adds `alg_hom.prod` to go with `alg_hom.fst` and `alg_hom.snd`. It was noticed to be missing during #16089.

src/algebra/algebra/basic.lean

@@ -713,6 +713,8 @@ lemma map_list_prod (s : list A) :
 
 section prod
 
+variables (R A B)
+
 /-- First projection as `alg_hom`. -/
 def fst : A × B →ₐ[R] A :=
 { commutes' := λ r, rfl, .. ring_hom.fst A B}
@@ -721,6 +723,33 @@ def fst : A × B →ₐ[R] A :=
 def snd : A × B →ₐ[R] B :=
 { commutes' := λ r, rfl, .. ring_hom.snd A B}
 
+variables {R A B}
+
+/-- The `pi.prod` of two morphisms is a morphism. -/
+@[simps] def prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : (A →ₐ[R] B × C) :=
+{ commutes' := λ r, by simp only [to_ring_hom_eq_coe, ring_hom.to_fun_eq_coe, ring_hom.prod_apply,
+    coe_to_ring_hom, commutes, algebra.algebra_map_prod_apply],
+  .. (f.to_ring_hom.prod g.to_ring_hom) }
+
+lemma coe_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : ⇑(f.prod g) = pi.prod f g := rfl
+
+@[simp] theorem fst_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
+  (fst R B C).comp (prod f g) = f := by ext; refl
+
+@[simp] theorem snd_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
+  (snd R B C).comp (prod f g) = g := by ext; refl
+
+@[simp] theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
+fun_like.coe_injective pi.prod_fst_snd
+
+/-- Taking the product of two maps with the same domain is equivalent to taking the product of
+their codomains. -/
+@[simps] def prod_equiv : ((A →ₐ[R] B) × (A →ₐ[R] C)) ≃ (A →ₐ[R] B × C) :=
+{ to_fun := λ f, f.1.prod f.2,
+  inv_fun := λ f, ((fst _ _ _).comp f, (snd _ _ _).comp f),
+  left_inv := λ f, by ext; refl,
+  right_inv := λ f, by ext; refl }
+
 end prod
 
 lemma algebra_map_eq_apply (f : A →ₐ[R] B) {y : R} {x : A} (h : algebra_map R A y = x) :