Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-02 12:52 f191f521

View on Github →

chore(algebra/big_operators): generalize map_prod to monoid_hom_class (#12354) This PR generalizes the following lemmas to (add_)monoid_hom_class:

  • map_prod, map_sum
  • map_multiset_prod, map_multiset_sum
  • map_list_prod, map_list_sum
  • map_finsupp_prod, map_finsupp_sum I haven't removed any of the existing specialized, namespaced versions of these lemmas yet, but I have marked them as protected and added a docstring saying to use the generic version instead.

Estimated changes

added theorem map_prod
deleted theorem monoid_hom.map_prod
deleted theorem mul_equiv.map_prod
deleted theorem ring_hom.map_list_prod
deleted theorem ring_hom.map_list_sum
deleted theorem ring_hom.map_multiset_sum
deleted theorem ring_hom.map_prod
deleted theorem ring_hom.map_sum
added theorem map_multiset_prod
modified theorem multiset.prod_hom'
modified theorem multiset.prod_hom
added theorem map_finsupp_prod
deleted theorem ring_hom.map_finsupp_prod
deleted theorem ring_hom.map_finsupp_sum
modified theorem list.prod_hom
modified theorem list.prod_map_hom
added theorem map_list_prod
deleted theorem monoid_hom.map_list_prod
added theorem unop_map_list_prod
deleted theorem polynomial.map_prod
deleted theorem polynomial.map_sum
deleted theorem filter.map_prod