mathlib

4568629f - chore(linear_algebra/tensor_product): generalize `tensor_tensor_tensor_comm_symm_tmul` (#18110)