Theorem TensorAlgebra.toDirectSum_ι

Modification history

2023-07-06 13:41

Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean

feat: port LinearAlgebra.TensorAlgebra.ToTensorPower (#4876)

Added TensorAlgebra.toDirectSum_ι View on Github →