Commit 2022-12-05 11:06 62ec8656

View on Github →

chore(algebra/big_operators/basic): golf results about bUnion (#17501) While the diff adds lines overall, these are new lemmas that were previously missing.

Estimated changes

Modified src/algebra/big_operators/basic.lean

Modified src/algebra/big_operators/ring.lean

Modified src/data/finset/basic.lean

added theorem finset.disj_Union_filter_eq_of_maps_to

Modified src/data/finset/powerset.lean

added theorem finset.pairwise_disjoint_powerset_len

added theorem finset.powerset_card_disj_Union

Modified src/data/finset/sigma.lean

added theorem finset.disj_Union_map_sigma_mk

added theorem finset.pairwise_disjoint_map_sigma_mk

Modified src/data/multiset/powerset.lean

deleted theorem multiset.disjoint_powerset_len

added theorem multiset.pairwise_disjoint_powerset_len