Commit 2026-02-23 20:15 d21cadec

View on Github →

feat(RingTheory/IsTensorProduct): heterogeneous associativity (#35557) We add a variant of TensorProduct.AlgebraTensorModule.assoc stated in terms of IsTensorProduct. From Pi1.

Estimated changes

Modified Mathlib/Algebra/Module/TransferInstance.lean

added def AddEquiv.linearEquiv

Modified Mathlib/RingTheory/IsTensorProduct.lean

added theorem IsTensorProduct.assocOfMapSMul_symm_tmul

added theorem IsTensorProduct.assocOfMapSMul_tmul

added theorem IsTensorProduct.assoc_symm_tmul

added theorem IsTensorProduct.assoc_tmul