hom): Add missing smul instances on add_monoid_hom (#6891)

Commit

4 years ago

feat(algebra/module/hom): Add missing smul instances on add_monoid_hom (#6891) These are defeq to the smul instances on `linear_map`, in `linear_algebra/basic.lean`.

Author

eric-wieser

Parents

a690ce77

mathlib3 396602bf - feat(algebra/module/hom): Add missing smul instances on add_monoid_hom (#6891)

mathlib3
396602bf - feat(algebra/module/hom): Add missing smul instances on add_monoid_hom (#6891)