function.injective.add_comm_group

Stream: maths

[Johan Commelin]

Should docs#function.injective.add_comm_group and it's monoid cousin be refactored to take gsmul (resp. nsmul) into account?

[Johan Commelin]

I think it's not dealt with automatically, right?

[Floris van Doorn]

Yes, if you care about the definitional behavior (diamonds) of gsmul/nsmul then you should add them.

[Eric Wieser]

I feel like to do what you suggest Johan we should probably have a has_gsmul class or similar to carry the data.