TheoremssameCycle, commute_iff, commute_iff', conj, eq_on_support_inter_nonempty_congr, eq_swap_of_apply_apply_eq_self, exists_pow_eq, exists_zpow_eq, extendDomain, inv, isConj, isConj_iff, isCycleOn, isCycle_pow_pos_of_lt_prime_order, ne_one, nonempty_support, of_pow, of_zpow, orderOf, pow_eq_one_iff, pow_eq_one_iff', pow_eq_one_iff'', pow_eq_pow_iff, pow_iff, sameCycle, sign, support_congr, support_pow_eq_iff, support_pow_of_pos_of_lt_orderOf, swap_mul, two_le_card_support, zpowersEquivSupport_apply, zpowersEquivSupport_symm_apply, apply_mem_iff, apply_ne, conj, countable, exists_pow_eq, exists_pow_eq', extendDomain, inv, isCycle_subtypePerm, of_inv, of_pow, of_zpow, pow_apply_eq, pow_apply_eq_pow_apply, pow_card_apply, range_pow, range_zpow, subsingleton, subtypePerm, zpow_apply_eq, zpow_apply_eq_zpow_apply, isCycle, apply_eq_self_iff, apply_left, apply_right, conj, eq_of_left, eq_of_right, equivalence, exists_fin_pow_eq, exists_nat_pow_eq, exists_pow_eq', exists_pow_eq'', extendDomain, inv, of_apply_left, of_apply_right, of_inv, of_pow, of_pow_left, of_pow_right, of_symm_apply_left, of_symm_apply_right, of_zpow, of_zpow_left, of_zpow_right, pow_left, pow_right, refl, rfl, subtypePerm, symm_apply_left, symm_apply_right, trans, zpow_left, zpow_right, cycle_zpow_mem_support_iff, isCycleOn_empty, isCycleOn_inv, isCycleOn_of_subsingleton, isCycleOn_one, isCycleOn_singleton, isCycleOn_swap, isCycle_iff_exists_isCycleOn, isCycle_iff_sameCycle, isCycle_inv, isCycle_swap, isCycle_swap_mul_aux₁, isCycle_swap_mul_aux₂, nodup_of_pairwise_disjoint_cycles, not_isCycle_one, sameCycle_apply_left, sameCycle_apply_right, sameCycle_comm, sameCycle_conj, sameCycle_extendDomain, sameCycle_inv, sameCycle_inv_apply_left, sameCycle_inv_apply_right, sameCycle_one, sameCycle_pow_left, sameCycle_pow_right, sameCycle_subtypePerm, sameCycle_symm_apply_left, sameCycle_symm_apply_right, sameCycle_zpow_left, sameCycle_zpow_right, subtypePerm_apply_pow_of_mem, subtypePerm_apply_zpow_of_mem, swap_isSwap_iff, zpow_eq_ofSubtype_subtypePerm_iff, exists_cycleOn, product_self_eq_disjiUnion_perm, product_self_eq_disjiUnion_perm_aux, sum_mul_sum_eq_sum_perm, sum_smul_sum_eq_sum_perm, addLeft_one_isCycle, addRight_one_isCycle, isCycleOn_formPerm, exists_cycleOn, isCycleOn_one, prod_self_eq_iUnion_perm | 135 |