mathlib

a7063ecc - feat(ring_theory/prod): ring homs to/from `R × S` (#2836)

feat(ring_theory/prod): ring homs to/from `R × S` (#2836) * move some instances from `algebra/pi_instances`; * add `prod.comm_semiring`; * define `ring_hom.fst`, `ring_hom.snd`, `ring_hom.prod`, and `ring_hom.prod_map`.