Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-27 08:57 a7063ecc

View on Github →

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.

Estimated changes

modified theorem monoid_hom.coe_prod_map
added theorem ring_hom.coe_fst
added theorem ring_hom.coe_prod_map
added theorem ring_hom.coe_snd
added def ring_hom.fst
added theorem ring_hom.fst_comp_prod
added theorem ring_hom.prod_apply
added theorem ring_hom.prod_map_def
added theorem ring_hom.prod_unique
added def ring_hom.snd
added theorem ring_hom.snd_comp_prod