Stream: PR reviews
Eric Wieser (Feb 05 2021 at 10:06):
I've just tried to put some multiplicative structures on
⨁ i, A i for cases like:
A iare submonoids of a larger semiring or comm_semiring
A iare subgroups of a larger ring or comm_semiring
⨂[R] (_ : fin i), M, aka the tensor powers
I initially created #5956 which addresses the first two of these cases, but then realized the third is also obviously useful, so generalized to #6053 which would enable supporting the third bullet in future.
Could I get some feedback on which of the two approaches looks better?
Eric Wieser (Feb 09 2021 at 23:56):
cc @Scott Morrison, who asked whether this thread existed on github
Johan Commelin (Feb 10 2021 at 18:53):
I'll try to find some time to think about these two PRs soonish
Last updated: May 06 2021 at 12:15 UTC