Mathlib Changelog
v4
Changelog
About
Github
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