mathlib

18562995 - feat(group_theory/perm/cycle/basic): Countable sets admit cycles (#17909)

feat(group_theory/perm/cycle/basic): Countable sets admit cycles (#17909) If `s` is countable, then there exists a permutation whose support is contained in `s` and which is a cycle on `s`.