right actions by nat on add_comm_monoids

Stream: general

[Eric Wieser]

Moving from another thread:

Jakob von Raumer said:

Now for add_comm_monoid we'd need a right action of ℕ on M, that doesen't seems unnatural either :unamused:

Yury G. Kudryashov said:

Will this create yet another diamond in case M = nat?

Yury G. Kudryashov said:

Because we already have an action of opposite nat on nat.

Yury G. Kudryashov said:

I wonder if there is a way to deal with these diamonds without adding lots of fields to monoid.

It does kind of feel like op_nsmul and op_zsmul fields are going to be unavoidable here, doesn't it...

[Jakob von Raumer]

Fields to what structure?

[Eric Wieser]

add_comm_monoid and add_comm_group

[Eric Wieser]

I don't know how we prevent to_additive adding uselesscomm_monoid.op_npow and comm_monoid.op_gpow fields at the same time though

[Notification Bot]

This topic was moved here from #maths > ideals in non-comm rings by Eric Wieser

[Jakob von Raumer]

Uh... but the other topic was far from being resolved :sweat_smile:

[Eric Wieser]

You can still post in that topic; I thought this would just draw more attention to the diamond issue on nat