Multiplication on direct_sum: #5956 and #6053

Stream: PR reviews

[Eric Wieser]

I've just tried to put some multiplicative structures on ⨁ i, A i for cases like:

• The A i are submonoids of a larger semiring or comm_semiring
• The A i are subgroups of a larger ring or comm_semiring
• The A i are ⨂[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]

cc @Scott Morrison, who asked whether this thread existed on github

[Johan Commelin]

I'll try to find some time to think about these two PRs soonish