mathlib3

6c8203f2 - chore(linear_algebra/bilinear_map): split off new file from linear_algebra/tensor_product (#9054)

chore(linear_algebra/bilinear_map): split off new file from linear_algebra/tensor_product (#9054) The first part of linear_algebra/tensor_product consisted of some basics on bilinear maps that are not directly related to the construction of the tensor product. This PR moves them to a new file.