Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-16 05:34 e7b8421e

View on Github →

chore(linear_algebra/finsupp): turn finsupp.lsum into add_equiv (#4597)

Estimated changes

Modified src/data/finsupp/basic.lean

deleted theorem finsupp.hom_ext

added theorem finsupp.lhom_ext'

added theorem finsupp.lhom_ext

added theorem finsupp.lift_add_hom_symm_apply_apply

Modified src/linear_algebra/direct_sum/finsupp.lean

modified def finsupp_lequiv_direct_sum

Modified src/linear_algebra/finsupp.lean

modified def finsupp.lsum

added theorem finsupp.lsum_symm_apply