Commit 2026-06-17 15:15 5ac74759
View on Github →chore(Analysis/SumIntegralComparisons): golf proofs (#40655)
Golfed the existing code in SumIntegralComparisons.lean. I had also added some additional API lemmas, but this is now done in #40588 and I have removed the redundant additions to simplify the PR.
