Theorem TensorPower.toTensorAlgebra_galgebra_toFun

Modification history

2023-07-06 13:41
Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
feat: port LinearAlgebra.TensorAlgebra.ToTensorPower (#4876)
Added TensorPower.toTensorAlgebra_galgebra_toFunView on Github →