Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 14:43 25c34e04

View on Github →

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_maps.

Estimated changes

modified def linear_map.smul_right
modified theorem linear_map.smul_right_apply