Commit 2022-04-18 19:11 3c20253b

View on Github →

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.

Estimated changes

Modified src/algebra/ring/pi.lean

Modified src/algebra/ring/prod.lean

modified theorem ring_hom.prod_comp_prod_map

modified def ring_hom.prod_map