Commit 2023-03-17 16:26 be34211e

View on Github →

feat: port GroupTheory.Perm.Cycle.Basic (#2528) Lotsa stuff to do, please help. Also, Equiv.Perm.Support should be named Equiv.Perm.support, right? I carried out that renaming in here.

Estimated changes

added theorem Equiv.Perm.IsCycle.inv
added theorem Equiv.Perm.cycleOf_inv
added theorem Equiv.Perm.cycleOf_one
added theorem Equiv.Perm.isCycle_inv
added theorem Finset.exists_cycleOn
modified theorem List.support_formPerm_le
modified theorem Equiv.Perm.Disjoint.mem_imp
modified theorem Equiv.Perm.Disjoint.mono
deleted def Equiv.Perm.Support
modified theorem Equiv.Perm.mem_support
modified theorem Equiv.Perm.not_mem_support
modified theorem Equiv.Perm.support_congr
modified theorem Equiv.Perm.support_inv
modified theorem Equiv.Perm.support_mul_le
modified theorem Equiv.Perm.support_one
modified theorem Equiv.Perm.support_pow_le
modified theorem Equiv.Perm.support_prod_le
modified theorem Equiv.Perm.support_refl
modified theorem Equiv.Perm.support_swap
modified theorem Equiv.Perm.support_swap_iff
modified theorem Equiv.Perm.support_zpow_le