Commit 2023-05-22 00:38 b284c7c0

View on Github →

feat: port GroupTheory.Perm.Cycle.Concrete (#3472)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

added def Cycle.formPerm

added theorem Cycle.formPerm_apply_mem_eq_next

added theorem Cycle.formPerm_coe

added theorem Cycle.formPerm_eq_self_of_not_mem

added theorem Cycle.formPerm_subsingleton

added theorem Cycle.isCycle_formPerm

added theorem Cycle.support_formPerm

added theorem Equiv.Perm.IsCycle.existsUnique_cycle

added theorem Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype

added theorem Equiv.Perm.IsCycle.existsUnique_cycle_subtype

added theorem Equiv.Perm.SameCycle.toList_isRotated

added theorem Equiv.Perm.formPerm_toList

added def Equiv.Perm.isoCycle'

added def Equiv.Perm.isoCycle

added theorem Equiv.Perm.length_toList

added theorem Equiv.Perm.length_toList_pos_of_mem_support

added theorem Equiv.Perm.mem_toList_iff

added theorem Equiv.Perm.next_toList_eq_apply

added theorem Equiv.Perm.nodup_toCycle

added theorem Equiv.Perm.nodup_toList

added theorem Equiv.Perm.nontrivial_toCycle

added theorem Equiv.Perm.nthLe_toList

added theorem Equiv.Perm.pow_apply_mem_toList_iff_mem_support

added def Equiv.Perm.toCycle

added theorem Equiv.Perm.toCycle_eq_toList

added def Equiv.Perm.toList

added theorem Equiv.Perm.toList_eq_nil_iff

added theorem Equiv.Perm.toList_formPerm_isRotated_self

added theorem Equiv.Perm.toList_formPerm_nil

added theorem Equiv.Perm.toList_formPerm_nontrivial

added theorem Equiv.Perm.toList_formPerm_singleton

added theorem Equiv.Perm.toList_ne_singleton

added theorem Equiv.Perm.toList_nthLe_zero

added theorem Equiv.Perm.toList_one

added theorem Equiv.Perm.toList_pow_apply_eq_rotate

added theorem Equiv.Perm.two_le_length_toList_iff_mem_support

added theorem List.cycleOf_formPerm

added theorem List.cycleType_formPerm

added theorem List.formPerm_apply_mem_eq_next

added theorem List.formPerm_disjoint_iff

added theorem List.isCycle_formPerm

added theorem List.pairwise_sameCycle_formPerm