mathlib

15f49ae2 - feat(linear_algebra/tensor_algebra/basic): add `tensor_algebra.tprod` (#14197)

feat(linear_algebra/tensor_algebra/basic): add `tensor_algebra.tprod` (#14197) This is related to `exterior_power.ι_multi`. Note the new import caused a proof to time out, so I squeezed the simps into term mode.