mathlib3

56ca12cc - feat(group_theory/perm/cycle/basic): Partition `s × s` into shifted diagonals (#17910)

feat(group_theory/perm/cycle/basic): Partition `s × s` into shifted diagonals (#17910) Given a cycle `f` on a finset `s`, we can partition the square `s ×ˢ s` into `(λ a, (a, (f ^ n) a)) '' s`, ranging over `n < card s`. This translates to an expansion of `∑ i in s, f i * ∑ i in s, g i` which is key to Chebyshev's sum inequality (#13187). For a finset with five elements, the picture looks like this: ``` 01234 40123 34012 23401 12340 ```