Commit 2023-11-27 14:14 1412ef2f
View on Github →feat(LinearAlgebra/TensorProduct): add liftAddHom (#8584)
This new TensorProduct.liftAddHom doesn't require bilinearity, only that scalar multiplication can be moved between the arguments.
In theory this could be used to golf some later definitions, but in practice this resulted in performance regressions (#8519).
For now we just leave a TODO, so that the performance/deduplication tradeoff doesn't hold up further mathematics.