Commit 2024-04-30 05:21 db6bc5d0

View on Github →

feat: More big operator lemmas (#10551) From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

added theorem Finset.prod_fiberwise_eq_prod_filter'

added theorem Finset.prod_fiberwise_eq_prod_filter

added theorem Finset.prod_sdiff_eq_prod_sdiff_iff

added theorem Finset.prod_sdiff_ne_prod_sdiff_iff

added theorem Finset.sum_card_fiberwise_eq_card_filter

added theorem Fintype.prod_boole

added theorem Fintype.prod_dite_eq'

added theorem Fintype.prod_dite_eq

added theorem Fintype.prod_ite_eq'

added theorem Fintype.prod_ite_eq

added theorem Fintype.prod_ite_eq_ite_exists

added theorem Fintype.prod_pi_mulSingle'

added theorem Fintype.prod_pi_mulSingle

added theorem Fintype.prod_subset

Modified Mathlib/Algebra/BigOperators/Ring.lean

added theorem Fintype.prod_add

added theorem Fintype.sum_mul_sum

added theorem Fintype.sum_pow

Modified Mathlib/Algebra/Module/BigOperators.lean

added theorem Fintype.sum_piFinset_apply

Modified Mathlib/Data/Finset/Basic.lean

modified theorem Finset.filter_eq_self

Modified Mathlib/Data/Finset/Union.lean

added theorem Finset.disjiUnion_filter_eq

modified theorem Finset.disjiUnion_filter_eq_of_maps_to

Modified Mathlib/Data/Fintype/BigOperators.lean

modified theorem Finset.card_pi

added theorem Fintype.card_filter_piFinset_const

added theorem Fintype.card_filter_piFinset_const_eq_of_mem

added theorem Fintype.card_filter_piFinset_eq

added theorem Fintype.card_filter_piFinset_eq_of_mem

modified theorem Fintype.card_pi

modified theorem Fintype.card_piFinset

Modified Mathlib/Data/Fintype/Pi.lean

added theorem Fintype.eval_image_piFinset_const

modified theorem Fintype.filter_piFinset_of_not_mem

added theorem Fintype.piFinset_update_eq_filter_piFinset_mem

added theorem Fintype.piFinset_update_singleton_eq_filter_piFinset_eq

Modified Mathlib/GroupTheory/PGroup.lean