Zulip Chat Archive

Stream: general

Topic: ideals in non-comm rings

Jakob von Raumer (Nov 04 2021 at 20:11):

It's still super hard to adapt that file. The annoying thing is that the most general conditions for the tensor product having a left action and having a right action are so asymmetric. There's one of the actions on M and N thats requirted to be a distrib_mul_action while the other one can be an arbitrary has_scalar, depending on whether it comes from tensor_product.left_has_scalar or from tensor_product.right_has_scalar, and these are of course not separate well in the current state of the file :tired:

Last updated: Aug 03 2023 at 10:10 UTC