Theorem IsTensorProduct.assoc_tmul

Modification history

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