Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-13 03:30 ec4bdab8

View on Github →

chore(group_theory/perm/cycle/basic): Move declarations around (#17906) Move the same_cycle lemmas before the is_cycle ones in order to reduce the diff in #17898.

Estimated changes

Modified src/group_theory/perm/cycle/basic.lean

modified theorem equiv.perm.is_cycle.eq_on_support_inter_nonempty_congr

modified theorem equiv.perm.is_cycle.mem_support_pos_pow_iff_of_lt_order_of

modified theorem equiv.perm.is_cycle.same_cycle

modified theorem equiv.perm.is_cycle.support_congr

modified theorem equiv.perm.is_cycle.support_pow_eq_iff

modified theorem equiv.perm.same_cycle.apply_eq_self_iff

modified theorem equiv.perm.same_cycle.nat''

modified theorem equiv.perm.same_cycle.nat'

modified theorem equiv.perm.same_cycle.symm

modified theorem equiv.perm.same_cycle.trans

modified theorem equiv.perm.same_cycle_apply

modified theorem equiv.perm.same_cycle_inv

modified theorem equiv.perm.same_cycle_inv_apply

modified theorem equiv.perm.same_cycle_pow_left_iff

modified theorem equiv.perm.same_cycle_zpow_left_iff