Hi all,

I'm trying to work on a cycle demposition of permutations in a similar way it's done in mathcomp library for transpositions.

For defining cycles themselves I would prefer to be able to give a list, again similar to your transpositions.

Is it already in the library?

`fconnect`

and `orbit`

defined in fingraph.v would be useful for that. I don't know whether their theory has been connected to that of symmetric groups.

There is `porbit`

in perm.v.

Ah, so I guess your problem is that `porbit`

does not return a list but a set (right?). Then using `traject`

seems to be a solution.

Well, rather that I want to define the cycles out of a list given by me (along with a proof of `uniq l`

).

So, you want to give a cycle as a list, and obtain a permutation that has the given cycle?

Yes!

And proving that all the permutations are a product of disjoint cycles, but this might be done with porbits I guess.

The function you want to prove injective would then be this one:

```
Definition fun_of_cycle (T : eqType) (xs : seq T) (x : T) : T :=
nth x (rot 1 xs) (index x xs).
```

Corresponds exactly to nth_uniq.

Surely, I'll be able to work myself the other part out.

Thx!

Last updated: Jul 15 2024 at 20:02 UTC