Commit 2023-07-27 23:50 0e849a1c

chore: split RingTheory/TensorProduct (#6187) There is a reasonably-sized section on modules over two rings before we actual reach tensor products of rings. The motivation for splitting here is to make room for the results in #6035. The declarations are copied without modification, the module docstring has been adapted.