Commit 2025-01-13 05:50 666dd637

View on Github →

chore: split Algebra/BigOperators/Group/{Multiset,Finset} (#20629) Follow on from #20625. Keeps only what is possible with the minimal imports required for the definitions themselves in the Defs file, and everything else moves to Lemmas.

Estimated changes

deleted theorem Equiv.Perm.prod_comp'
deleted theorem Equiv.Perm.prod_comp
deleted theorem Equiv.prod_comp
deleted theorem Finset.op_sum
deleted theorem Finset.prod_attach_univ
deleted theorem Finset.prod_bij'
deleted theorem Finset.prod_bij
deleted theorem Finset.prod_bijective
deleted theorem Finset.prod_const_one
deleted theorem Finset.prod_dite_irrel
deleted theorem Finset.prod_div_distrib
deleted theorem Finset.prod_empty
deleted theorem Finset.prod_equiv
deleted theorem Finset.prod_erase_attach
deleted theorem Finset.prod_hom_rel
deleted theorem Finset.prod_induction
deleted theorem Finset.prod_int_mod
deleted theorem Finset.prod_inv_distrib
deleted theorem Finset.prod_ite_index
deleted theorem Finset.prod_ite_irrel
deleted theorem Finset.prod_map
deleted theorem Finset.prod_map_val
deleted theorem Finset.prod_mem_multiset
deleted theorem Finset.prod_mk
deleted theorem Finset.prod_nat_mod
deleted theorem Finset.prod_nbij'
deleted theorem Finset.prod_nbij
deleted theorem Finset.prod_of_isEmpty
deleted theorem Finset.prod_pow
deleted theorem Finset.prod_range_zero
deleted theorem Finset.prod_to_list
deleted theorem Finset.prod_val
deleted theorem Finset.prod_zpow
deleted theorem Finset.sum_int_mod
deleted theorem Finset.sum_nat_mod
deleted theorem Finset.unop_sum
deleted theorem Fintype.prod_bijective
deleted theorem Fintype.prod_empty
deleted theorem Fintype.prod_equiv
deleted theorem Multiset.card_sum
deleted theorem Multiset.count_sum'
deleted theorem Units.coe_prod
deleted theorem map_prod
deleted theorem ofAdd_list_prod
deleted theorem ofAdd_multiset_prod
deleted theorem ofAdd_sum
deleted theorem ofMul_list_prod
deleted theorem ofMul_multiset_prod
deleted theorem ofMul_prod
deleted theorem toAdd_list_sum
deleted theorem toAdd_multiset_sum
deleted theorem toAdd_prod
deleted theorem toMul_list_sum
deleted theorem toMul_multiset_sum
deleted theorem toMul_sum
added theorem Equiv.Perm.prod_comp'
added theorem Equiv.Perm.prod_comp
added theorem Equiv.prod_comp
added theorem Finset.op_sum
added theorem Finset.prod_bij'
added theorem Finset.prod_bij
added theorem Finset.prod_bijective
added theorem Finset.prod_const_one
added theorem Finset.prod_dite_irrel
added theorem Finset.prod_empty
added theorem Finset.prod_equiv
added theorem Finset.prod_hom_rel
added theorem Finset.prod_induction
added theorem Finset.prod_int_mod
added theorem Finset.prod_ite_index
added theorem Finset.prod_ite_irrel
added theorem Finset.prod_map
added theorem Finset.prod_map_val
added theorem Finset.prod_mk
added theorem Finset.prod_nat_mod
added theorem Finset.prod_nbij'
added theorem Finset.prod_nbij
added theorem Finset.prod_of_isEmpty
added theorem Finset.prod_pow
added theorem Finset.prod_range_zero
added theorem Finset.prod_to_list
added theorem Finset.prod_val
added theorem Finset.prod_zpow
added theorem Finset.sum_int_mod
added theorem Finset.sum_nat_mod
added theorem Finset.unop_sum
added theorem Fintype.prod_bijective
added theorem Fintype.prod_empty
added theorem Fintype.prod_equiv
added theorem Multiset.card_sum
added theorem Multiset.count_sum'
added theorem Units.coe_prod
added theorem map_prod
added theorem ofAdd_list_prod
added theorem ofAdd_multiset_prod
added theorem ofAdd_sum
added theorem ofMul_list_prod
added theorem ofMul_multiset_prod
added theorem ofMul_prod
added theorem toAdd_list_sum
added theorem toAdd_multiset_sum
added theorem toAdd_prod
added theorem toMul_list_sum
added theorem toMul_multiset_sum
added theorem toMul_sum
deleted theorem Multiset.pow_count
deleted def Multiset.prod
deleted theorem Multiset.prod_coe
deleted theorem Multiset.prod_cons
deleted theorem Multiset.prod_eq_foldl
deleted theorem Multiset.prod_eq_foldr
deleted theorem Multiset.prod_hom_rel
deleted theorem Multiset.prod_induction
deleted theorem Multiset.prod_map_one
deleted theorem Multiset.prod_pair
deleted theorem Multiset.prod_replicate
deleted theorem Multiset.prod_singleton
deleted theorem Multiset.prod_toList
deleted theorem Multiset.prod_zero
added theorem Multiset.pow_count
added def Multiset.prod
added theorem Multiset.prod_coe
added theorem Multiset.prod_cons
added theorem Multiset.prod_eq_foldl
added theorem Multiset.prod_eq_foldr
added theorem Multiset.prod_hom_rel
added theorem Multiset.prod_map_one
added theorem Multiset.prod_pair
added theorem Multiset.prod_toList
added theorem Multiset.prod_zero