Commit 2024-06-26 13:40 4f99ec07

View on Github →

feat(GroupTheory/Perm/Cycle/Factors): Remove finiteness requirement from cycleOf. (#13145) cycleOf can be defined using only a decidability condition, rather than the current finiteness condition (from which decidability can be inferred). This commit removes this dependency on finiteness.

Estimated changes

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

modified theorem Equiv.Perm.Disjoint.cycleOf_mul_distrib

modified theorem Equiv.Perm.SameCycle.exists_pow_eq

modified theorem Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support

modified theorem Equiv.Perm.SameCycle.mem_support_iff

modified theorem Equiv.Perm.card_support_cycleOf_pos_iff

modified def Equiv.Perm.cycleOf

modified theorem Equiv.Perm.cycleOf_apply

modified theorem Equiv.Perm.cycleOf_apply_apply_pow_self

modified theorem Equiv.Perm.cycleOf_apply_apply_self

modified theorem Equiv.Perm.cycleOf_apply_apply_zpow_self

modified theorem Equiv.Perm.cycleOf_apply_self

modified theorem Equiv.Perm.cycleOf_eq_one_iff

modified theorem Equiv.Perm.cycleOf_inv

modified theorem Equiv.Perm.cycleOf_mul_of_apply_right_eq_self

modified theorem Equiv.Perm.cycleOf_one

modified theorem Equiv.Perm.cycleOf_pow_apply_self

modified theorem Equiv.Perm.cycleOf_self_apply

modified theorem Equiv.Perm.cycleOf_self_apply_pow

modified theorem Equiv.Perm.cycleOf_self_apply_zpow

modified theorem Equiv.Perm.cycleOf_zpow_apply_self

modified theorem Equiv.Perm.isCycleOn_support_cycleOf

modified theorem Equiv.Perm.isCycle_cycleOf

modified theorem Equiv.Perm.isCycle_cycleOf_iff

modified theorem Equiv.Perm.mem_support_cycleOf_iff'

modified theorem Equiv.Perm.mem_support_cycleOf_iff

modified theorem Equiv.Perm.pow_mod_card_support_cycleOf_self_apply

modified theorem Equiv.Perm.pow_mod_orderOf_cycleOf_apply

modified theorem Equiv.Perm.support_cycleOf_eq_nil_iff

modified theorem Equiv.Perm.support_cycleOf_le

modified theorem Equiv.Perm.support_cycleOf_nonempty

modified theorem Equiv.Perm.two_le_card_support_cycleOf_iff