mathlib

97a63eaa - feat(linear_algebra/matrix/to_lin): add `linear_map.to_matrix_distrib_mul_action_to_linear_map` (#17337)

feat(linear_algebra/matrix/to_lin): add `linear_map.to_matrix_distrib_mul_action_to_linear_map` (#17337) This is a generalization of the result for `algebra.lsmul`. `linear_map.to_matrix_lsmul` is generalized too. Stating the result with `matrix.diagonal (λ _, x)` is more insightful than doing so with an `ite`.