mathlib

8b858d0b - feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid (#3490)

feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid (#3490) The extra `_`s required to make this still build are unfortunate, but hopefully someone else can work out how to remove them in a later PR. Co-authored-by: Mario Carneiro <di.gama@gmail.com>