Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-13 23:34 103c1ffa

View on Github →

feat(data/(d)finsupp): (d)finsupp.update (#9015)

Estimated changes

Modified src/data/dfinsupp.lean

added theorem dfinsupp.coe_update

added theorem dfinsupp.support_update

added theorem dfinsupp.support_update_ne_zero

added def dfinsupp.update

added theorem dfinsupp.update_eq_erase

added theorem dfinsupp.update_self

Modified src/data/finsupp/basic.lean

added theorem finsupp.coe_update

added theorem finsupp.support_update

added theorem finsupp.support_update_ne_zero

added theorem finsupp.support_update_zero

added def finsupp.update

added theorem finsupp.update_self