Commit 2022-05-23 10:20 15f49ae2
View on Github →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.