Commit 2025-02-27 07:23 832d9990

View on Github →

chore: split long file Mathlib.LinearAlgebra.TensorProduct.Basic (#22351)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Modified Mathlib/Data/Matrix/Kronecker.lean

Created Mathlib/LinearAlgebra/TensorProduct/Associator.lean

added theorem LinearMap.lid_comp_rTensor

added theorem LinearMap.rTensor_tensor

added theorem TensorProduct.assoc_symm_tmul

added theorem TensorProduct.assoc_tmul

added def TensorProduct.leftComm

added theorem TensorProduct.leftComm_symm_tmul

added theorem TensorProduct.leftComm_tmul

added def TensorProduct.lidOfCompatibleSMul

added theorem TensorProduct.lidOfCompatibleSMul_tmul

added theorem TensorProduct.lid_eq_rid

added theorem TensorProduct.lid_symm_apply

added theorem TensorProduct.lid_tmul

added theorem TensorProduct.map_map_assoc

added theorem TensorProduct.map_map_assoc_symm

added theorem TensorProduct.map_map_comp_assoc_eq

added theorem TensorProduct.map_map_comp_assoc_symm_eq

added theorem TensorProduct.rid_symm_apply

added theorem TensorProduct.rid_tmul

added def TensorProduct.tensorTensorTensorAssoc

added theorem TensorProduct.tensorTensorTensorAssoc_symm_tmul

added theorem TensorProduct.tensorTensorTensorAssoc_tmul

added def TensorProduct.tensorTensorTensorComm

added theorem TensorProduct.tensorTensorTensorComm_comp_map

added theorem TensorProduct.tensorTensorTensorComm_symm

added theorem TensorProduct.tensorTensorTensorComm_tmul

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

deleted theorem LinearMap.lid_comp_rTensor

deleted theorem LinearMap.rTensor_tensor

deleted theorem TensorProduct.assoc_symm_tmul

deleted theorem TensorProduct.assoc_tmul

deleted def TensorProduct.leftComm

deleted theorem TensorProduct.leftComm_symm_tmul

deleted theorem TensorProduct.leftComm_tmul

deleted def TensorProduct.lidOfCompatibleSMul

deleted theorem TensorProduct.lidOfCompatibleSMul_tmul

deleted theorem TensorProduct.lid_eq_rid

deleted theorem TensorProduct.lid_symm_apply

deleted theorem TensorProduct.lid_tmul

deleted theorem TensorProduct.map_map_assoc

deleted theorem TensorProduct.map_map_assoc_symm

deleted theorem TensorProduct.map_map_comp_assoc_eq

deleted theorem TensorProduct.map_map_comp_assoc_symm_eq

deleted theorem TensorProduct.rid_symm_apply

deleted theorem TensorProduct.rid_tmul

deleted def TensorProduct.tensorTensorTensorAssoc

deleted theorem TensorProduct.tensorTensorTensorAssoc_symm_tmul

deleted theorem TensorProduct.tensorTensorTensorAssoc_tmul

deleted def TensorProduct.tensorTensorTensorComm

deleted theorem TensorProduct.tensorTensorTensorComm_comp_map

deleted theorem TensorProduct.tensorTensorTensorComm_symm

deleted theorem TensorProduct.tensorTensorTensorComm_tmul

Modified Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

Modified Mathlib/RingTheory/Coalgebra/Basic.lean