mathlib

e303a7d9 - feat(linear_algebra/tensor_product): tensoring linear maps with modules (#4771)