Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 05:57 56f6c8e8

View on Github →

chore(algebra/big_operators/intervals): Move and golf sum_range_sub_sum_range (#13359) Move sum_range_sub_sum_range to a better file. Also implemented the golf demonstrated in this paper https://arxiv.org/pdf/2202.01344.pdf from @spolu.

Estimated changes