mathlib3

6791ed9b - chore(algebra/module/linear_map): add linear_map.to_distrib_mul_action_hom (#6573)

chore(algebra/module/linear_map): add linear_map.to_distrib_mul_action_hom (#6573) My aim in adding this is primarily to give the reader a hint that `distrib_mul_action_hom` exists. The only difference between the two is that `linear_map` can infer `map_zero'` from its typeclass arguments.