feat(linear_algebra/tensor_product): Generalise tensor product to non-commutative rings

[javra]

Replaces linear_algebra.tensor_product by a whole folder of files, generalising it to non-commutative rings and isolating everything that depends on the left action on the tensor product. A file containing the corresponding right action can be added in future.

---

Still quite a lot of work to do, I haven't fixed any of the files importing linear_algebra.tensor_product and we will likely need to create or presume instances for is_symmetric_smul in some cases.