Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-19 22:45 accc50ed

View on Github →

chore(data/finsupp): to_additive on on_finset_sum (#4698)

Estimated changes