Zulip Chat Archive

Stream: maths

Topic: pow

view this post on Zulip Johan Commelin (Mar 27 2019 at 18:13):

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.

view this post on Zulip Chris Hughes (Mar 27 2019 at 18:16):

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

Last updated: May 06 2021 at 19:30 UTC