Creating a example `perm`

Stream: Is there code for X?

[Ben]

I am trying to create a exemplar instance of a perm. How can I write a invertible bijective function over a finite type, e.g. one that in cycle notion is written as (1 3 4 2)? I want to pass it to cycle_factors

[Eric Wieser]

https://leanprover-community.github.io/mathlib_docs/group_theory/perm/concrete_cycle.html might be what you're after, in particular the c[1, 3, 4, 2] notation

[Yakov Pechersky]

And if you don't want the notation (which is limited to fintypes, and your example doesn't specify, which implies nat), you can always use list.form_perm [1, 3, 4, 2].