mathlib
mathlib copied to clipboard
feat(linear_algebra/tensor_product): Generalise tensor product to non-commutative rings
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.