Tensor products of modules

[Alizter]

Once we have #1921, we should define right modules and then the tensor product of a right module and a left module.

We can also try to show it is symmetric monoidal. (For commutative rings or bimodules).

We should also think about generalising Dan and Luis' characterization of the universal property of the tensor product of abelian groups as precomposition with the AbHom being an equivalence. I have a formalization of general AbHoms in an additive category that will be finished soon so we could use that.

This should correspond to the classical notion of "R-balanced maps". We should check.