mathlib

a008b33f - feat(data/finsupp/to_dfinsupp): add sigma_finsupp_lequiv_dfinsupp (#7818)

feat(data/finsupp/to_dfinsupp): add sigma_finsupp_lequiv_dfinsupp (#7818) Equivalences between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. - [x] depends on: #7819 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>