Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-11 21:18 a008b33f

View on Github →

feat(data/finsupp/to_dfinsupp): add sigma_finsupp_lequiv_dfinsupp (#7818) Equivalences between (Σ i, η i) →₀ N and Π₀ i, (η i →₀ N).

depends on: #7819

Estimated changes

Modified src/data/finsupp/to_dfinsupp.lean

added def sigma_finsupp_add_equiv_dfinsupp

added def sigma_finsupp_equiv_dfinsupp

added theorem sigma_finsupp_equiv_dfinsupp_add

added theorem sigma_finsupp_equiv_dfinsupp_apply

added theorem sigma_finsupp_equiv_dfinsupp_smul

added theorem sigma_finsupp_equiv_dfinsupp_support

added theorem sigma_finsupp_equiv_dfinsupp_symm_apply

added def sigma_finsupp_lequiv_dfinsupp