Commit 2024-02-23 00:32 ad2c78f5

View on Github →

refactor(Data/Finsupp): Make Finsupp.filter computable (#8979) This doesn't have any significant downstream fallout, and removes some subsingleton elimination from one or two proofs. This enables some trivial computations on factorizations, eg finding the odd prime factors:

/-- info: fun₀ | 3 => 2 | 5 => 1 -/
#guard_msgs in
#eval (Nat.factorization 720).filter Odd

Zulip thread

Estimated changes

modified def Finsupp.filter
modified def Finsupp.filterAddHom
modified theorem Finsupp.filter_add
modified theorem Finsupp.filter_apply
modified theorem Finsupp.filter_curry
modified theorem Finsupp.filter_eq_indicator
modified theorem Finsupp.filter_eq_sum
modified theorem Finsupp.filter_neg
modified theorem Finsupp.filter_sub
modified theorem Finsupp.filter_sum
modified theorem Finsupp.support_filter
modified theorem Finsupp.range_restrictDom
modified def Finsupp.restrictDom
modified theorem Finsupp.restrictDom_apply