feat(linear_algebra/tensor_product): define `tensor_tensor_tensor_comm` (#7724)
feat(linear_algebra/tensor_product): define `tensor_tensor_tensor_comm` (#7724)

The intended application is defining the bracket structure when extending the scalars of a Lie algebra.





leanprover-community/mathlib,leanprover-community/mathlib