chore(algebra/ring/{pi, prod}): fix errors in ring_hom for pi and prod. (#13501)

Looks like some things were incorrectly changed when copied from the corresponding `monoid_hom` files.

Author: j-loreaux

src/algebra/ring/pi.lean

@@ -100,7 +100,7 @@ section ring_hom
 universes u v
 variable {I : Type u}
 
-/-- Evaluation of functions into an indexed collection of monoids at a point is a monoid
+/-- Evaluation of functions into an indexed collection of rings at a point is a ring
 homomorphism. This is `function.eval` as a `ring_hom`. -/
 @[simps]
 def pi.eval_ring_hom (f : I → Type v) [Π i, non_assoc_semiring (f i)] (i : I) :

src/algebra/ring/prod.lean

@@ -120,14 +120,14 @@ variables [non_assoc_semiring R'] [non_assoc_semiring S'] [non_assoc_semiring T]
 variables (f : R →+* R') (g : S →+* S')
 
 /-- `prod.map` as a `ring_hom`. -/
-def prod_map : R × S →* R' × S' := (f.comp (fst R S)).prod (g.comp (snd R S))
+def prod_map : R × S →+* R' × S' := (f.comp (fst R S)).prod (g.comp (snd R S))
 
 lemma prod_map_def : prod_map f g = (f.comp (fst R S)).prod (g.comp (snd R S)) := rfl
 
 @[simp]
 lemma coe_prod_map : ⇑(prod_map f g) = prod.map f g := rfl
 
-lemma prod_comp_prod_map (f : T →* R) (g : T →* S) (f' : R →* R') (g' : S →* S') :
+lemma prod_comp_prod_map (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') :
   (f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
 rfl