mathlib
bcd5cd37 - feat(algebra/pointwise): add to_additive attributes for pointwise smul (#8878)

Commit

4 years ago

feat(algebra/pointwise): add to_additive attributes for pointwise smul (#8878) I wanted this to generalize some definitions in #2819 but it should be independent.

Author

alexjbest

Parents

bb4026f4

mathlib bcd5cd37 - feat(algebra/pointwise): add to_additive attributes for pointwise smul (#8878)

mathlib
bcd5cd37 - feat(algebra/pointwise): add to_additive attributes for pointwise smul (#8878)