Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-29 12:50 91604cbe

View on Github →

feat(data/finsupp/to_dfinsupp): add equivalences between finsupp and dfinsupp (#7311) A rework of #7217, that adds a more elementary equivalence.

Estimated changes

Created src/data/finsupp/to_dfinsupp.lean

added def dfinsupp.to_finsupp

added theorem dfinsupp.to_finsupp_add

added theorem dfinsupp.to_finsupp_coe

added theorem dfinsupp.to_finsupp_neg

added theorem dfinsupp.to_finsupp_single

added theorem dfinsupp.to_finsupp_smul

added theorem dfinsupp.to_finsupp_sub

added theorem dfinsupp.to_finsupp_support

added theorem dfinsupp.to_finsupp_to_dfinsupp

added theorem dfinsupp.to_finsupp_zero

added def finsupp.to_dfinsupp

added theorem finsupp.to_dfinsupp_add

added theorem finsupp.to_dfinsupp_coe

added theorem finsupp.to_dfinsupp_neg

added theorem finsupp.to_dfinsupp_single

added theorem finsupp.to_dfinsupp_smul

added theorem finsupp.to_dfinsupp_sub

added theorem finsupp.to_dfinsupp_to_finsupp

added theorem finsupp.to_dfinsupp_zero

added def finsupp_equiv_dfinsupp

added theorem to_dfinsupp_support

Modified src/linear_algebra/direct_sum/finsupp.lean