Commit 2023-04-07 16:43 cdb0c707

View on Github →

feat: port GroupTheory.Perm.Fin (#3288)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Perm/Fin.lean

added theorem Equiv.Perm.decomposeFin.symm_sign

added def Equiv.Perm.decomposeFin

added theorem Equiv.Perm.decomposeFin_symm_apply_one

added theorem Equiv.Perm.decomposeFin_symm_apply_succ

added theorem Equiv.Perm.decomposeFin_symm_apply_zero

added theorem Equiv.Perm.decomposeFin_symm_of_one

added theorem Equiv.Perm.decomposeFin_symm_of_refl

added theorem Fin.coe_cycleRange_of_le

added theorem Fin.coe_cycleRange_of_lt

added def Fin.cycleRange

added theorem Fin.cycleRange_apply

added theorem Fin.cycleRange_last

added theorem Fin.cycleRange_of_eq

added theorem Fin.cycleRange_of_gt

added theorem Fin.cycleRange_of_le

added theorem Fin.cycleRange_of_lt

added theorem Fin.cycleRange_self

added theorem Fin.cycleRange_succAbove

added theorem Fin.cycleRange_symm_succ

added theorem Fin.cycleRange_symm_zero

added theorem Fin.cycleRange_zero'

added theorem Fin.cycleRange_zero

added theorem Fin.cycleType_cycleRange

added theorem Fin.isCycle_cycleRange

added theorem Fin.isThreeCycle_cycleRange_two

added theorem Fin.sign_cycleRange

added theorem Fin.succAbove_cycleRange

added theorem Finset.univ_perm_fin_succ

added theorem cycleType_finRotate

added theorem cycleType_finRotate_of_le

added theorem finRotate_succ_eq_decomposeFin

added theorem isCycle_finRotate

added theorem isCycle_finRotate_of_le

added theorem sign_finRotate

added theorem support_finRotate

added theorem support_finRotate_of_le