Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-13 00:53 87c1820c

View on Github →

feat(group_theory/perm/concrete_cycle): perms from cycle data structure (#8866)

Estimated changes

Modified src/group_theory/perm/concrete_cycle.lean

added def cycle.form_perm

added theorem cycle.form_perm_apply_mem_eq_next

added theorem cycle.form_perm_coe

added theorem cycle.form_perm_eq_form_perm_iff

added theorem cycle.form_perm_eq_self_of_not_mem

added theorem cycle.form_perm_reverse

added theorem cycle.form_perm_subsingleton

added theorem cycle.is_cycle_form_perm

added theorem cycle.support_form_perm