Commit 2025-01-25 06:17 62560ab2

View on Github →

feat: two Finset lemmas (#15294) Add prod_image_of_disjoint (and the to_additive version sum_image_of_disjoint) and sUnion_disjiUnion

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

added theorem Finset.prod_filter_of_pairwise_eq_one

added theorem Finset.prod_image_of_disjoint

added theorem Finset.prod_image_of_pairwise_eq_one

Modified Mathlib/Data/Finset/Union.lean

added theorem Finset.sUnion_disjiUnion