## Stream: math-comp users

### Topic: Cycles

#### Raul (Mar 13 2023 at 22:40):

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?

#### Kazuhiko Sakaguchi (Mar 13 2023 at 22:48):

`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.

#### Kazuhiko Sakaguchi (Mar 13 2023 at 22:49):

There is `porbit` in perm.v.

#### Kazuhiko Sakaguchi (Mar 13 2023 at 22:58):

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.

#### Raul (Mar 13 2023 at 23:00):

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

#### Kazuhiko Sakaguchi (Mar 13 2023 at 23:08):

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

Yes!

#### Raul (Mar 13 2023 at 23:10):

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

#### Kazuhiko Sakaguchi (Mar 13 2023 at 23:23):

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).
``````

#### Raul (Mar 13 2023 at 23:34):

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