mathlib

05f7e8dc - 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.