Zulip Chat Archive

Stream: PR reviews

Topic: Multiplication on direct_sum: #5956 and #6053


Eric Wieser (Feb 05 2021 at 10:06):

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 (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: Dec 20 2023 at 11:08 UTC