to_dfinsupp): add equivalences between finsupp and dfinsupp (#7311)

Commit

4 years ago

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

Author

eric-wieser

Parents