ideals in non-comm rings

Stream: general

[Jakob von Raumer]

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: