Theorem IsTensorProduct.assocOfMapSMul_symm_tmul

Modification history

2026-02-23 20:15
Mathlib/RingTheory/IsTensorProduct.lean
feat(RingTheory/IsTensorProduct): heterogeneous associativity (#35557) …
Added IsTensorProduct.assocOfMapSMul_symm_tmulView on Github →