Theorem TensorProduct.fromDirectLimit_of_tmul

Modification history

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