mathlib

12bb9aee - chore(linear_algebra/*): split lines and doc `direct_sum/tensor_product` (#6360)

chore(linear_algebra/*): split lines and doc `direct_sum/tensor_product` (#6360) This PR provides a short module doc to `direct_sum/tensor_product` (the file contains only one result). Furthermore, it splits lines in the `linear_algebra` folder. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>