compare different actions

Stream: new members

[Winston Yin]

I'm trying to consider two different group actions of G on A as examples of mul_action. If I define both as instances, then when I write g • a, it would not be clear which of the two actions it refers to. Does that mean I should just write def action1 ... : mul_action G A and def action2 ... : mul_action G A, and use the .smul g a method of each?

[Winston Yin]

When I write theorems about the two mul_actions, would I then have to explicitly provide (ma1 ma2 : mul_action G A) as variables?

[Scott Morrison]

Don't consider two different actions of G. Instead introduce a type synonym for one of the actions.

[Winston Yin]

Could you elaborate on type synonym pls?

[Eric Wieser]

An example would be mul_action (opposite M) M (docs#opposite.monoid.to_opposite_mul_action) vs mul_action M M (docs#monoid.to_mul_action)

[Eric Wieser]

Here docs#opposite is the synonym