Equiv.Perm.toList vs Function.periodicOrbit

Stream: mathlib4

[Yury G. Kudryashov]

I've just noticed that docs#Equiv.Perm.toList and docs#Function.periodicOrbit are almost the same with a few differences:

• the former is computatble
• the former needs an Equiv.Perm on a Fintype (to ensure that every point is periodic);
• the former gives a docs#List, not docs#Cycle.

Should we sync APIs?

[Yakov Pechersky]

There is also docs#Equiv.Perm.toCycle

[Yakov Pechersky]

The fintype + computability also comes from the need to compute the "minimal period" which is in condition inside periodicOrbit

[Yury G. Kudryashov]

I suggest that we

• split the file about periodic orbits;
• add a version of periodicOrbit that gives a List, not a Cycle;
• make Equiv.Perm code use it for proofs while using the same computable definition.