Theorem TensorProduct.toDirectLimit_tmul_of

Modification history

2023-12-12 07:30
Mathlib/Algebra/Module/DirectLimitAndTensorProduct.lean
feat : direct limit and tensor product commutes (#8473) …
Added TensorProduct.toDirectLimit_tmul_ofView on Github →