Commit 2022-11-07 03:20 97a63eaa
View on Github →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.