Commit 2025-12-11 10:09 02a656ba
View on Github →feat(LinearAlgebra/PiTensorProduct): add version of subsingletonEquiv for dependent case (#32598)
Dependent PiTensorProducts over singleton types occur naturally when
using tmulEquivDep to split off one index from a dependent
PiTensorProduct. This PR creates subsingletonEquivDep to deal with
this situation.
The non-dependent subsingletonEquiv is re-defined as a specialization
of the general case. This changes the definition of toDirectSum_ι in
TensorAlgebra/ToTensorPower, and so its proof is therefore changed.
