Commit 2023-01-18 18:14 bc61efff

View on Github →

chore: revert Multiset and Finset API to use Prop instead of Bool (#1652)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

modified theorem Finset.prod_filter_mul_prod_filter_not

Modified Mathlib/Algebra/FreeMonoid/Count.lean

modified def FreeAddMonoid.count

modified def FreeAddMonoid.countp

modified def FreeMonoid.count

modified def FreeMonoid.countp

modified theorem FreeMonoid.countp_of'

modified theorem FreeMonoid.countp_of

Modified Mathlib/Algebra/GCDMonoid/Finset.lean

Modified Mathlib/Combinatorics/SetFamily/Compression/Down.lean

Modified Mathlib/Data/Finset/Basic.lean

modified theorem Finset.disjoint_filter

modified theorem Finset.disjoint_filter_filter'

modified theorem Finset.disjoint_filter_filter

modified theorem Finset.disjoint_filter_filter_neg

added theorem Finset.filter_False

added theorem Finset.filter_True

deleted theorem Finset.filter_false

deleted theorem Finset.filter_true

modified theorem Finset.filter_union_filter_neg_eq

modified theorem Finset.monotone_filter_right

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.filter_card_add_filter_neg_card_eq_card

Modified Mathlib/Data/Finset/Fold.lean

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

Modified Mathlib/Data/Finset/Prod.lean

modified theorem Finset.disjoint_diag_offDiag

modified theorem Finset.filter_product

modified theorem Finset.filter_product_card

modified theorem Finset.filter_product_left

modified theorem Finset.filter_product_right

Modified Mathlib/Data/Fintype/Basic.lean

modified theorem Finset.coe_filter_univ

modified theorem Finset.compl_filter

Modified Mathlib/Data/Multiset/Basic.lean

modified theorem Multiset.coe_count

modified def Multiset.count

modified theorem Multiset.count_eq_card_filter_eq

modified theorem Multiset.count_filter

modified theorem Multiset.count_filter_of_neg

modified theorem Multiset.count_filter_of_pos

modified theorem Multiset.count_zero

added theorem Multiset.countp_False

added theorem Multiset.countp_True

modified theorem Multiset.countp_congr

modified theorem Multiset.countp_eq_countp_filter_add

deleted theorem Multiset.countp_false

modified theorem Multiset.countp_map

deleted theorem Multiset.countp_true

modified theorem Multiset.filterMap_eq_filter

modified theorem Multiset.filter_add_filter

modified theorem Multiset.filter_congr

modified theorem Multiset.filter_filter

added theorem Multiset.map_count_True_eq_filter_card

deleted theorem Multiset.map_count_true_eq_filter_card

modified theorem Multiset.monotone_filter_right

Modified Mathlib/Data/Multiset/Nodup.lean

modified theorem Multiset.Nodup.filter

Modified Mathlib/GroupTheory/Perm/Support.lean