Commit 2023-07-06 13:41 8793f093

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean

added def TensorAlgebra.equivDirectSum

added theorem TensorAlgebra.mk_reindex_cast

added theorem TensorAlgebra.mk_reindex_fin_cast

added def TensorAlgebra.ofDirectSum

added theorem TensorAlgebra.ofDirectSum_comp_toDirectSum

added theorem TensorAlgebra.ofDirectSum_of_tprod

added theorem TensorAlgebra.ofDirectSum_toDirectSum

added def TensorAlgebra.toDirectSum

added theorem TensorAlgebra.toDirectSum_comp_ofDirectSum

added theorem TensorAlgebra.toDirectSum_ofDirectSum

added theorem TensorAlgebra.toDirectSum_tensorPower_tprod

added theorem TensorAlgebra.toDirectSum_ι

added theorem TensorPower.list_prod_gradedMonoid_mk_single

added def TensorPower.toTensorAlgebra

added theorem TensorPower.toTensorAlgebra_gMul

added theorem TensorPower.toTensorAlgebra_gOne

added theorem TensorPower.toTensorAlgebra_galgebra_toFun

added theorem TensorPower.toTensorAlgebra_tprod