Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-25 21:27 49af34d9

View on Github →

feat(group_theory/perm/cycles): same_cycle and cycle_of lemmas (#8835)

Estimated changes

Modified src/group_theory/perm/cycles.lean

added theorem equiv.perm.card_support_cycle_of_pos_iff

added theorem equiv.perm.cycle_of_self_apply

added theorem equiv.perm.cycle_of_self_apply_gpow

added theorem equiv.perm.cycle_of_self_apply_pow

added theorem equiv.perm.pow_mod_card_support_cycle_of_self_apply

added theorem equiv.perm.same_cycle.cycle_of_eq

added theorem equiv.perm.same_cycle.mem_support_iff

modified theorem equiv.perm.same_cycle.symm

modified theorem equiv.perm.same_cycle.trans

added theorem equiv.perm.same_cycle_gpow_left_iff

added theorem equiv.perm.support_cycle_of_le

added theorem equiv.perm.two_le_card_support_cycle_of_iff