module): add `is_scalar_tower` and `smul_comm_class` instances for `continuous_linear_map` (#10375)

Commit

4 years ago

feat(topology/algebra/module): add `is_scalar_tower` and `smul_comm_class` instances for `continuous_linear_map` (#10375) Also generalize some instances about `smul`.

Author

urkud

Parents

0d09e993

mathlib 96540719 - feat(topology/algebra/module): add `is_scalar_tower` and `smul_comm_class` instances for `continuous_linear_map` (#10375)

mathlib
96540719 - feat(topology/algebra/module): add `is_scalar_tower` and `smul_comm_class` instances for `continuous_linear_map` (#10375)