Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-07 03:49 5eb19182

View on Github →

feat(group_theory/perm/concrete_cycle): is_cycle_form_perm (#8859)

Estimated changes

Created src/group_theory/perm/concrete_cycle.lean

added theorem list.cycle_of_form_perm

added theorem list.cycle_type_form_perm

added theorem list.form_perm_apply_mem_eq_next

added theorem list.form_perm_disjoint_iff

added theorem list.is_cycle_form_perm

added theorem list.pairwise_same_cycle_form_perm

Modified src/group_theory/perm/list.lean

deleted theorem list.form_perm_apply_not_mem

added theorem list.form_perm_eq_self_of_not_mem

deleted theorem list.form_perm_ne_self_imp_mem

added theorem list.mem_of_form_perm_ne_self