6.1 Cycle representation of permutations
For a permutation \(\sigma \in \mathfrak {S}_{n}\), the cycle count \(c(\sigma )\) is the number of cycles in the disjoint-cycle decomposition of \(\sigma \). In MathComp this is the cardinality of \(\mathrm{porbits}(\sigma )\), the set of orbits of \(\sigma \) acting on \(\{ 0, \dots , n-1\} \) by iteration.
Every cycle is non-empty, so the cycle count is bounded by \(n\).
Each fixed point is a 1-cycle, so \(c(\mathrm{id}) = n\).