Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-27 03:31 bcd5cd37

View on Github →

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.

Estimated changes