Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-25 07:39 e8187ac1

View on Github →

feat(category/preadditive): comp_sum (#3162) Adds lemmas to distribute composition over finset.sum, in a preadditive category.

Estimated changes