Commit 2023-10-26 16:24 645da3e5

View on Github →

feat (GroupTheory.Perm.Cycle.PossibleTypes) : cycleTypes of perm (#7433) Characterize the possible types of permutations: given m : Multiset ℕ, there are permutations in Equiv.Perm α with cycleType m if and only if m.sumis at most Fintype.card α and the members of m are at least 2. This result will be used in later PR which computes the cardinality of conjugacy classes in Equiv.Perm α and alternatingGroup α

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fintype/Card.lean

added theorem List.exists_pw_disjoint_with_card

Modified Mathlib/Data/List/Basic.lean

added theorem List.disjoint_map

added theorem List.disjoint_pmap

Modified Mathlib/Data/List/Join.lean

added theorem List.sublist_join

Modified Mathlib/Data/List/Range.lean

added theorem List.mem_mem_ranges_iff_lt_sum

added def List.ranges

added theorem List.ranges_disjoint

added theorem List.ranges_join

added theorem List.ranges_length

added theorem List.ranges_nodup

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

added theorem Equiv.Perm.exists_with_cycleType_iff