Commit 2024-10-16 03:49 90f515bc

View on Github →

chore: move List.permutations material out of List.Perm (#17795) This moves some material off the longest pole.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/List.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Data/Fintype/List.lean

Modified Mathlib/Data/Fintype/Perm.lean

Modified Mathlib/Data/List/Perm.lean

deleted theorem List.Perm.permutations'

deleted theorem List.Perm.permutations

deleted theorem List.count_permutations'Aux_self

deleted theorem List.getElem_permutations'Aux

deleted theorem List.get_permutations'Aux

deleted theorem List.injective_permutations'Aux

deleted theorem List.length_permutations'Aux

deleted theorem List.length_permutations

deleted theorem List.length_permutationsAux

deleted theorem List.mem_permutations'

deleted theorem List.mem_permutations

deleted theorem List.mem_permutationsAux_of_perm

deleted theorem List.mem_permutations_of_perm_lemma

deleted theorem List.nodup_permutations'Aux_iff

deleted theorem List.nodup_permutations'Aux_of_not_mem

deleted theorem List.nodup_permutations

deleted theorem List.nodup_permutations_iff

deleted theorem List.perm_of_mem_permutations

deleted theorem List.perm_of_mem_permutationsAux

added theorem List.perm_option_toList

deleted theorem List.perm_option_to_list

deleted theorem List.perm_permutations'Aux_comm

deleted theorem List.perm_permutations'_iff

deleted theorem List.perm_permutations_iff

deleted theorem List.permutations'Aux_get_zero

deleted theorem List.permutations_perm_permutations'

deleted theorem List.permutations_take_two

Modified Mathlib/Data/List/Permutation.lean

added theorem List.Perm.permutations'

added theorem List.Perm.permutations

added theorem List.count_permutations'Aux_self

added theorem List.getElem_permutations'Aux

added theorem List.get_permutations'Aux

added theorem List.injective_permutations'Aux

added theorem List.length_permutations'Aux

added theorem List.length_permutations

added theorem List.length_permutationsAux

added theorem List.mem_permutations'

added theorem List.mem_permutations

added theorem List.mem_permutationsAux_of_perm

added theorem List.mem_permutations_of_perm_lemma

added theorem List.nodup_permutations'Aux_iff

added theorem List.nodup_permutations'Aux_of_not_mem

added theorem List.nodup_permutations

added theorem List.nodup_permutations_iff

added theorem List.perm_of_mem_permutations

added theorem List.perm_of_mem_permutationsAux

added theorem List.perm_permutations'Aux_comm

added theorem List.perm_permutations'_iff

added theorem List.perm_permutations_iff

added theorem List.permutations'Aux_get_zero

added theorem List.permutations_perm_permutations'

added theorem List.permutations_take_two

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean