Commit 2023-01-10 13:41 b8683232

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.