feat(group_theory/perm/cycle/basic): Cycle on a set (#17899)
Define `equiv.perm.is_cycle_on`, a predicate for a permutation to be a cycle on a set.
This has two discrepancies with the existing `equiv.perm.is_cycle_on` (apart from the obvious one that `is_cycle_on` is restricted to a set):
* `is_cycle_on` forbids fixed points (on `s`) while `is_cycle` allows them.
* `is_cycle` forbids the identity while `is_cycle_on` allows it.
I think the first one isn't so bad given that `is_cycle` is meant to be used over the entire type (so you can't just rule out fixed points). The second one is more of a worry as I had to case-split on `s.subsingleton ∨ s.nontrivial` in several `is_cycle_on` lemmas to derive them from the corresponding `is_cycle` ones, while of course the `is_cycle` ones would also have held for a weaker version of `is_cycle` that allows the identity.
