mathlib

f784cc61 - feat(linear_algebra/tensor_product/matrix): connect with `matrix.kronecker` (#18616)

feat(linear_algebra/tensor_product/matrix): connect with `matrix.kronecker` (#18616) This shows that `to_matrix _ _ (tensor_product.map f g) = to_matrix _ _ f ⊗ₖ to_matrix _ _ g` , and the equivalent statement for `to_lin`.