Commit 2024-03-04 10:56 5925ea9b

View on Github →

chore(GroupTheory/Perm/Cycle/Basic): Split (#10907) The file Mathlib.GroupTheory.Perm.Cycle.Basic was too big and this PR splits it in several components:

  • Mathlib.GroupTheory.Perm.Cycle.Basic contains everything related to a permutation being a cycle,
  • Mathlib.GroupTheory.Perm.Cycle.Factors is about the cycles of a permutation and the decomposition of a permutation into disjoint cycles
  • Mathlib.GroupTheory.Perm.Closure contains generation results for the permutation groups
  • Mathlib.GroupTheory.Perm.Finite contains general results specific to permutation of finite types I moved some results to Mathlib.GroupTheory.Perm.Support I also moved some results from Mathlib.GroupTheory.Perm.Sign to Mathlib.GroupTheory.Perm.Finite Some imports could be reduced, and the shake linter required a few adjustments in some other.

Estimated changes

deleted def Equiv.Perm.cycleOf
deleted theorem Equiv.Perm.cycleOf_apply
deleted theorem Equiv.Perm.cycleOf_inv
deleted theorem Equiv.Perm.cycleOf_one
deleted theorem Equiv.Perm.support_conj
modified theorem Finset.exists_cycleOn
added theorem Equiv.Perm.cycleOf_inv
added theorem Equiv.Perm.cycleOf_one
modified def Equiv.Perm.modSwap