Commit 2021-01-17 00:33 dec44fe7

chore(group_theory/perm/{sign,cycles}): renaming for dot notation, linting, formatting (#5777) Declarations renamed in group_theory/perm/sign.lean (all of these are under equiv.perm):

• disjoint_mul_comm -> disjoint.mul_comm
• disjoint_mul_left -> disjoint.mul_left
• disjoint_mul_right -> disjoint.mul_right
• is_swap_of_subtype -> is_swap.of_subtype_is_swap
• sign_eq_of_is_swap -> is_swap.sign_eq Declarations renamed in group_theory/perm/cycles.lean (all of these are under equiv.perm):
• is_cycle_swap -> is_cycle.swap
• is_cycle_inv -> is_cycle.inv
• exists_gpow_eq_of_is_cycle -> is_cycle.exists_gpow_eq
• exists_pow_eq_of_is_cycle -> is_cycle.exists_pow_eq
• eq_swap_of_is_cycle_of_apply_apply_eq_self -> eq_swap_of_apply_apply_eq_self
• is_cycle_swap_mul -> is_cycle.swap_mul
• sign_cycle -> is_cycle.sign
• apply_eq_self_iff_of_same_cycle -> same_cycle.apply_eq_self_iff
• same_cycle_of_is_cycle -> is_cycle.same_cycle
• cycle_of_apply_of_same_cycle -> same_cycle.cycle_of_apply
• cycle_of_cycle -> is_cycle.cycle_of_eq I also added a basic module doc string to group_theory/perm/cycles.lean.