mathlib3
a6d445db - feat(data/finsupp): Add `map_finsupp_prod` to homs (#4585)

Commit

5 years ago

feat(data/finsupp): Add `map_finsupp_prod` to homs (#4585) This is a convenience alias for `map_prod`, which is awkward to use.

References

Author

eric-wieser

Parents