mathlib3

dec44fe7 - chore(group_theory/perm/{sign,cycles}): renaming for dot notation, linting, formatting (#5777)

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`.