mathlib

3b2c97f9 - feat(data/dfinsupp): Port `finsupp.lsum` and lemmas about `lift_add_hom` (#4833)

feat(data/dfinsupp): Port `finsupp.lsum` and lemmas about `lift_add_hom` (#4833) This then removes the proofs of any `direct_sum` lemmas which become equivalent to the `lift_add_hom` lemmas