Commit 2025-08-24 17:03 835057f8

View on Github →

chore(Multiset,Finset): add filter_true/filter_false (#28838)

  • Add Multiset.filter_true and Multiset.filter_false.
  • Rename Finset.filter_True to Finset.filter_true.
  • Rename Finset.filter_False to Finset.filter_false.
  • Add @[simp] to filter_true/filter_false/filter_eq_self/filter_eq_nil.

Estimated changes

deleted theorem Finset.Finset.filter_True
added theorem Multiset.filter_false
added theorem Multiset.filter_true