mathlib

0dca20a2 - feat(data/(d)finsupp): update_eq_sub_add_single (#9184)

feat(data/(d)finsupp): update_eq_sub_add_single (#9184) Also with `erase_eq_sub_single`. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>