mathlib

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

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.