Commit 2023-04-05 09:20 2be86d83

View on Github →

feat: port GroupTheory.Perm.Cycle.Type (#3027)

Estimated changes

Modified Mathlib.lean

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

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

added theorem Equiv.Perm.Disjoint.cycleType

added theorem Equiv.Perm.IsCycle.cycleType

added theorem Equiv.Perm.IsSwap.mul_mem_closure_three_cycles

added theorem Equiv.Perm.IsThreeCycle.card_support

added theorem Equiv.Perm.IsThreeCycle.cycleType

added theorem Equiv.Perm.IsThreeCycle.inv

added theorem Equiv.Perm.IsThreeCycle.inv_iff

added theorem Equiv.Perm.IsThreeCycle.isCycle

added theorem Equiv.Perm.IsThreeCycle.isThreeCycle_sq

added theorem Equiv.Perm.IsThreeCycle.orderOf

added theorem Equiv.Perm.IsThreeCycle.sign

added def Equiv.Perm.IsThreeCycle

added theorem Equiv.Perm.VectorsProdEqOne.card

added def Equiv.Perm.VectorsProdEqOne.equivVector

added theorem Equiv.Perm.VectorsProdEqOne.mem_iff

added theorem Equiv.Perm.VectorsProdEqOne.one_eq

added def Equiv.Perm.VectorsProdEqOne.rotate

added theorem Equiv.Perm.VectorsProdEqOne.rotate_length

added theorem Equiv.Perm.VectorsProdEqOne.rotate_rotate

added theorem Equiv.Perm.VectorsProdEqOne.rotate_zero

added def Equiv.Perm.VectorsProdEqOne.vectorEquiv

added theorem Equiv.Perm.VectorsProdEqOne.zero_eq

added theorem Equiv.Perm.card_compl_support_modEq

added theorem Equiv.Perm.card_cycleType_eq_one

added theorem Equiv.Perm.card_cycleType_eq_zero

added theorem Equiv.Perm.card_cycleType_pos

added def Equiv.Perm.cycleType

added theorem Equiv.Perm.cycleType_conj

added theorem Equiv.Perm.cycleType_def

added theorem Equiv.Perm.cycleType_eq'

added theorem Equiv.Perm.cycleType_eq

added theorem Equiv.Perm.cycleType_eq_zero

added theorem Equiv.Perm.cycleType_extendDomain

added theorem Equiv.Perm.cycleType_inv

added theorem Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinset

added theorem Equiv.Perm.cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub

added theorem Equiv.Perm.cycleType_ofSubtype

added theorem Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two

added theorem Equiv.Perm.cycleType_one

added theorem Equiv.Perm.cycleType_prime_order

added theorem Equiv.Perm.dvd_of_mem_cycleType

added theorem Equiv.Perm.exists_fixed_point_of_prime'

added theorem Equiv.Perm.exists_fixed_point_of_prime

added theorem Equiv.Perm.filter_parts_partition_eq_cycleType

added theorem Equiv.Perm.isConj_iff_cycleType_eq

added theorem Equiv.Perm.isConj_of_cycleType_eq

added theorem Equiv.Perm.isCycle_of_prime_order''

added theorem Equiv.Perm.isCycle_of_prime_order'

added theorem Equiv.Perm.isCycle_of_prime_order

added theorem Equiv.Perm.isThreeCycle_swap_mul_swap_same

added theorem Equiv.Perm.lcm_cycleType

added theorem Equiv.Perm.le_card_support_of_mem_cycleType

added theorem Equiv.Perm.mem_cycleType_iff

added theorem Equiv.Perm.one_lt_of_mem_cycleType

added theorem Equiv.Perm.orderOf_cycleOf_dvd_orderOf

added def Equiv.Perm.partition

added theorem Equiv.Perm.partition_eq_of_isConj

added theorem Equiv.Perm.parts_partition

added theorem Equiv.Perm.sign_of_cycleType'

added theorem Equiv.Perm.sign_of_cycleType

added theorem Equiv.Perm.subgroup_eq_top_of_swap_mem

added theorem Equiv.Perm.sum_cycleType

added theorem Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles

added theorem Equiv.Perm.two_dvd_card_support

added theorem Equiv.Perm.two_le_of_mem_cycleType

added def Equiv.Perm.vectorsProdEqOne

added theorem card_support_eq_three_iff

added theorem exists_prime_addOrderOf_dvd_card

added theorem exists_prime_orderOf_dvd_card

Modified Mathlib/GroupTheory/Perm/Support.lean

added theorem Equiv.Perm.Disjoint.conj

added theorem Equiv.Perm.disjoint_conj