Commit 2021-09-16 11:34 86d20e51

View on Github →

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.

Estimated changes

Modified src/data/dfinsupp.lean

modified theorem dfinsupp.coe_smul

added theorem dfinsupp.filter_add

added def dfinsupp.filter_add_monoid_hom

added def dfinsupp.filter_linear_map

added theorem dfinsupp.filter_neg

added theorem dfinsupp.filter_smul

added theorem dfinsupp.filter_sub

added theorem dfinsupp.filter_zero

modified theorem dfinsupp.mk_smul

modified theorem dfinsupp.single_smul

modified theorem dfinsupp.smul_apply

added def dfinsupp.subtype_domain_linear_map

added theorem dfinsupp.subtype_domain_smul

Modified src/linear_algebra/dfinsupp.lean