Zulip Chat Archive

Stream: general

Topic: finsupp scalar diamond


Neil Strickland (Jun 10 2019 at 11:12):

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?


Last updated: Dec 20 2023 at 11:08 UTC