mathlib

33ea6980 - feat(linear_algebra/tensor_product): characterise range of tensor product of two linear maps (#7340)