mathlib

86d20e51 - feat(data/dfinsupp): add arithmetic lemmas about filter (#9175)

feat(data/dfinsupp): add arithmetic lemmas about filter (#9175) This adds `dfinsupp.filter_{zero,add,neg,sub,smul}` and `dfinsupp.subtype_domain_smul`, along with some bundled maps. This also cleans up some variable explicitness.