Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes