Theorem TensorProduct.directLimitLeft_rTensor_of

Modification history

2025-01-02 19:57
Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean
feat(Algebra/Colimit): the directed system of finitely generated submodules (#20264) …
Added TensorProduct.directLimitLeft_rTensor_ofView on Github →