finsupp scalar diamond

Stream: general

[Neil Strickland]

It seems that there are two ways to make finsupp α ℤ into a ℤ-module, one via add_comm_group.module and the other via finsupp.module, and that these are not defeq. Is there a standard way to deal with this?