Skip to content

Commit

Permalink
chore(group_theory/perm/{sign,cycles}): renaming for dot notation, li…
Browse files Browse the repository at this point in the history
…nting, 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`.
  • Loading branch information
bryangingechen committed Jan 17, 2021
1 parent a2630fc commit dec44fe
Show file tree
Hide file tree
Showing 2 changed files with 236 additions and 181 deletions.

0 comments on commit dec44fe

Please sign in to comment.