mathlib3

25c34e04 - refactor(linear_algebra,algebra/algebra): generalize `linear_map.smul_right` (#5967)

refactor(linear_algebra,algebra/algebra): generalize `linear_map.smul_right` (#5967) * the new `linear_map.smul_right` generalizes both the old `linear_map.smul_right` and the old `linear_map.smul_algebra_right`; * add `smul_comm_class` for `linear_map`s.