Commit 2025-05-29 15:17 ec35a548

View on Github →

feat(LinearAlgebra/TensorProduct): make AlgebraTensorModule.* defeq to the regular version (#25298)

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Associator.lean

added theorem TensorProduct.comm_trans_lid

added theorem TensorProduct.comm_trans_rid

added def TensorProduct.rightComm

added theorem TensorProduct.rightComm_symm

added theorem TensorProduct.rightComm_tmul

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

modified def TensorProduct.uncurry

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.assoc_eq

added theorem TensorProduct.AlgebraTensorModule.leftComm_eq

added theorem TensorProduct.AlgebraTensorModule.map_eq

modified theorem TensorProduct.AlgebraTensorModule.rid_eq_rid

added theorem TensorProduct.AlgebraTensorModule.rightComm_eq