Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 16:11 0dca20a2

View on Github →

feat(data/(d)finsupp): update_eq_sub_add_single (#9184) Also with erase_eq_sub_single.

Estimated changes

Modified src/algebra/group/pi.lean

added theorem pi.update_eq_sub_add_single

Modified src/data/dfinsupp.lean

added theorem dfinsupp.erase_eq_sub_single

added theorem dfinsupp.update_eq_erase_add_single

added theorem dfinsupp.update_eq_single_add_erase

added theorem dfinsupp.update_eq_sub_add_single

Modified src/data/finsupp/basic.lean

added theorem finsupp.erase_eq_sub_single

added theorem finsupp.update_eq_erase_add_single

added theorem finsupp.update_eq_single_add_erase

added theorem finsupp.update_eq_sub_add_single