Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-04 07:58 863f0075

View on Github →

feat(data/list/basic): map_permutations (#8188) As requested on Zulip.

Estimated changes

Modified src/data/list/basic.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_bind

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_aux2_append

added theorem list.permutations_aux2_fst

added theorem list.permutations_aux2_snd_cons

added theorem list.permutations_aux2_snd_nil

Modified src/data/list/perm.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.mem_foldr_permutations_aux2

deleted theorem list.mem_permutations_aux2'

deleted theorem list.mem_permutations_aux2

deleted theorem list.permutations_aux2_append

deleted theorem list.permutations_aux2_fst

deleted theorem list.permutations_aux2_snd_cons

deleted theorem list.permutations_aux2_snd_nil