Commit 2023-06-04 08:38 6f6b64f4

View on Github →

feat: port LinearAlgebra.TensorPower (#4648)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/TensorPower.lean

added theorem PiTensorProduct.gradedMonoid_eq_of_reindex_cast

added def TensorPower.algebraMap₀

added theorem TensorPower.algebraMap₀_eq_smul_one

added theorem TensorPower.algebraMap₀_mul

added theorem TensorPower.algebraMap₀_mul_algebraMap₀

added theorem TensorPower.algebraMap₀_one

added def TensorPower.cast

added theorem TensorPower.cast_cast

added theorem TensorPower.cast_eq_cast

added theorem TensorPower.cast_refl

added theorem TensorPower.cast_symm

added theorem TensorPower.cast_tprod

added theorem TensorPower.cast_trans

added theorem TensorPower.gMul_def

added theorem TensorPower.gMul_eq_coe_linearMap

added theorem TensorPower.gOne_def

added theorem TensorPower.galgebra_toFun_def

added theorem TensorPower.gradedMonoid_eq_of_cast

added def TensorPower.mulEquiv

added theorem TensorPower.mul_algebraMap₀

added theorem TensorPower.mul_assoc

added theorem TensorPower.mul_one

added theorem TensorPower.one_mul

added theorem TensorPower.tprod_mul_tprod

added def TensorPower