Commit 2024-01-10 10:28 b8dc3667

View on Github →

chore: Relocate big operator lemmas (#9383) A bunch of lemmas in Algebra.BigOperators.Ring were not about rings. This PR moves them along with some lemmas from Data.Fintype.BigOperators to their correct place. I create a new file with the content from #6605 to avoid importing Fin material in finset files as a result. From LeanAPAP

Estimated changes

modified theorem Finset.prod_attach
added theorem Finset.prod_powerset
added theorem Finset.prod_univ_pi
modified theorem Finset.dvd_sum
modified theorem Finset.mul_sum
modified theorem Finset.prod_add
modified theorem Finset.prod_add_ordered
modified theorem Finset.prod_natCast
modified theorem Finset.prod_one_sub_ordered
deleted theorem Finset.prod_powerset
modified theorem Finset.prod_sub_ordered
modified theorem Finset.prod_sum
added theorem Finset.prod_univ_sum
modified theorem Finset.sum_boole_mul
modified theorem Finset.sum_div
modified theorem Finset.sum_mul
modified theorem Finset.sum_mul_boole
modified theorem Finset.sum_mul_sum
added theorem Finset.sum_pow'
deleted theorem pos_div_pow_pos
added theorem Fin.mem_piFinset_succ'
added theorem Fin.mem_piFinset_succ
deleted theorem Finset.prod_attach_univ
deleted theorem Finset.prod_univ_pi
deleted theorem Finset.prod_univ_sum
deleted theorem Fin.mem_piFinset_succ_iff
deleted theorem NNReal.sum_div