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





leanprover-community/mathlib,leanprover-community/mathlib