pow

Stream: maths

[Johan Commelin]

In #850 I'm PRing mul_action and distrib_mul_action. These are rather low-level classes wrapping around has_scalar and smul.
Somehow there is a very analogous theory for has_pow and pow. I haven't fleshed out the details. Somehow it is not as easy as a to_additive, because pow encodes an action on the right. I wonder whether it is useful to build some generic structure here that generalises all the gpow, fpow, rpow things that we currently have.
It would be good if some clone of to_additive could do a bunch of lifting.

[Chris Hughes]

I think fpow and rpow probably don't fit into nice classes, because 0^-n doesn't make sense.