mathlib

d1723c04 - refactor(group_theory/perm/cycle/basic): Consolidate API (#17898)

refactor(group_theory/perm/cycle/basic): Consolidate API (#17898) Reorganise and complete the cycle API: * Previously, `is_cycle` was spelling out the definition of `same_cycle`. Now use it explicitly. * Change binder to semi-implicit in the definition of `is_cycle`. * Add lemmas and iff aliases. * Golf existing proofs using those (mostly invisible from the diff because git decided I am moving the `is_cycle` API) * Improve lemma names, mostly for better dot notation. ## New lemmas * `maps_to.extend_domain` * `surj_on.extend_domain` * `bij_on.extend_domain` * `extend_domain_pow` * `extend_domain_zpow` * `same_cycle.rfl` * `eq.same_cycle` * `same_cycle.conj` * `same_cycle_conj` * `same_cycle_pow_right_iff` * `same_cycle_zpow_right_iff` * `same_cycle.pow_left` * `same_cycle.pow_right` * `same_cycle.zpow_left` * `same_cycle.zpow_left` * `same_cycle.of_pow` * `same_cycle.of_zpow` * `same_cycle_subtype_perm` * `same_cycle.subtype_perm` * `same_cycle_extend_domain` * `is_cycle.conj` * `is_cycle.pow_eq_one_iff'` * `is_cycle.pow_eq_one_iff''` ## Renames * `order_of_is_cycle` → `is_cycle.order_of` * `is_cycle.is_cycle_conj` → `is_cycle.conj` * `is_cycle_of_is_cycle_pow` → `is_cycle.of_pow` * `is_cycle_of_is_cycle_zpow` → `is_cycle.of_zpow` * `same_cycle_cycle` → `is_cycle_iff_same_cycle` * `mem_support_pos_pow_iff_of_lt_order_of` → `support_pow_of_pos_of_lt_order_of` and change the statement to talk about unextensionalised finset equality