Johan Commelin (Mar 27 2019 at 18:13):
In #850 I'm PRing
distrib_mul_action. These are rather low-level classes wrapping around
Somehow there is a very analogous theory for
pow. I haven't fleshed out the details. Somehow it is not as easy as a
pow encodes an action on the right. I wonder whether it is useful to build some generic structure here that generalises all the
rpow things that we currently have.
It would be good if some clone of
to_additive could do a bunch of lifting.
Chris Hughes (Mar 27 2019 at 18:16):
rpow probably don't fit into nice classes, because
0^-n doesn't make sense.
Last updated: May 06 2021 at 19:30 UTC