Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-27 14:05 c9a81b00

View on Github →

refactor(*): unify API of list/multiset/finset.prod_hom (#1820)

  • refactor(*): unify API of list/multiset/finset.prod_hom Also remove is_group_hom.map_prod; use *.prod_hom.symm or monoid_hom.map_*prod instead.
  • Update src/ring_theory/ideal_operations.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • Restore explicit args of list.fold(l/r)_hom
  • Fix group_theory/perm/sign
  • Fix quadratic_reciprocity
  • Fix compile

Estimated changes

modified theorem finset.prod_hom
deleted theorem is_group_hom.map_prod
added theorem monoid_hom.map_prod
added theorem complex.exp_list_sum
added theorem complex.exp_sum
added theorem real.exp_list_sum
added theorem real.exp_multiset_sum
added theorem real.exp_sum
modified theorem list.foldl_hom
modified theorem list.foldl_map
modified theorem list.foldr_hom
modified theorem list.foldr_map
added theorem list.prod_hom
added theorem list.prod_hom_rel
modified theorem multiset.prod_hom
added theorem multiset.prod_hom_rel
deleted theorem multiset.sum_hom
added theorem nnreal.coe_list_prod
added theorem nnreal.coe_list_sum
added theorem nnreal.coe_prod
added theorem nnreal.coe_sum
deleted theorem nnreal.prod_coe
deleted theorem nnreal.sum_coe