Commit 2020-10-30 08:20 03a477c4
View on Github →feat(data/dfinsupp): Port over the finsupp.lift_add_hom API (#4821)
These lemmas are mostly copied with minimal translation from finsupp.
A few proofs are taken from direct_sum.
The API of direct_sum is deliberately unchanged in this PR.