Commit 2024-10-09 19:42 78d00773
View on Github →feat(Algebra/BigOperators/Group): add sum_tsub_distrib (#17130)
Upstreamed from https://github.com/b-mehta/ExponentialRamsey/blob/7e17b629a915a082869f494c8afa56a3e1c7a88d/ExponentialRamsey/Prereq/Mathlib/Algebra/BigOperators/Ring.lean#L17