how to define this permu

Stream: new members

[vxctyxeha]

image.png

[Philippe Duchon]

Not sure what the details should be, but it looks like
Mathlib.GroupTheory.Perm.Cycle.Concrete should have what you're looking for (defining your $\sigma$ as the $\ell$-th power of the cyclic permutation that maps each integer to the next one, modulo $k+\ell$.

(it should also be simpler to go against the usual mathematical practice and use Fin n, or at least naturals $0$ to $n-1$ instead of $1$ to $n$)