Orbit-size multiset identity

The multiset of orbit sizes of a permutation π : Equiv.Perm (Fin n) equals its cycle type plus singleton fixed-point orbits.

Helper lemmas

Main theorem

theorem RS.orbCard_multiset {n : ℕ} (π : Equiv.Perm (Fin n)) : Multiset.map (orbCard π) Finset.univ.val = π.cycleType + Multiset.replicate (n - π.cycleType.sum) 1

The orbit sizes are the cycle type together with a singleton per fixed point.