Commit 2021-10-18 05:53 6cd6ff44

View on Github →

split(data/list/permutation): split off data.list.basic (#9749) This moves all the list.permutations definitions and lemmas not involving list.perm to a new file.

Estimated changes

Modified src/data/list/basic.lean

deleted theorem list.foldr_permutations_aux2

deleted theorem list.length_foldr_permutations_aux2'

deleted theorem list.length_foldr_permutations_aux2

deleted theorem list.length_permutations_aux2

deleted theorem list.map_map_permutations'_aux

deleted theorem list.map_map_permutations_aux2

deleted theorem list.map_permutations'

deleted theorem list.map_permutations

deleted theorem list.map_permutations_aux2'

deleted theorem list.map_permutations_aux2

deleted theorem list.map_permutations_aux

deleted theorem list.mem_foldr_permutations_aux2

deleted theorem list.mem_permutations_aux2'

deleted theorem list.mem_permutations_aux2

deleted theorem list.permutations'_aux_eq_permutations_aux2

deleted theorem list.permutations_append

deleted theorem list.permutations_aux2_append

deleted theorem list.permutations_aux2_comp_append

deleted theorem list.permutations_aux2_fst

deleted theorem list.permutations_aux2_snd_cons

deleted theorem list.permutations_aux2_snd_eq

deleted theorem list.permutations_aux2_snd_nil

deleted theorem list.permutations_aux_append

deleted theorem list.permutations_aux_cons

deleted theorem list.permutations_aux_nil

deleted theorem list.permutations_nil

Modified src/data/list/defs.lean

Modified src/data/list/perm.lean

Created src/data/list/permutation.lean

added theorem list.foldr_permutations_aux2

added theorem list.length_foldr_permutations_aux2'

added theorem list.length_foldr_permutations_aux2

added theorem list.length_permutations_aux2

added theorem list.map_map_permutations'_aux

added theorem list.map_map_permutations_aux2

added theorem list.map_permutations'

added theorem list.map_permutations

added theorem list.map_permutations_aux2'

added theorem list.map_permutations_aux2

added theorem list.map_permutations_aux

added theorem list.mem_foldr_permutations_aux2

added theorem list.mem_permutations_aux2'

added theorem list.mem_permutations_aux2

added theorem list.permutations'_aux_eq_permutations_aux2

added theorem list.permutations_append

added theorem list.permutations_aux2_append

added theorem list.permutations_aux2_comp_append

added theorem list.permutations_aux2_fst

added theorem list.permutations_aux2_snd_cons

added theorem list.permutations_aux2_snd_eq

added theorem list.permutations_aux2_snd_nil

added theorem list.permutations_aux_append

added theorem list.permutations_aux_cons

added theorem list.permutations_aux_nil

added theorem list.permutations_nil