Commit 2023-01-10 12:25 99b6ebcc

View on Github →

feat: port Data.List.Permutation (#1445)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Defs.lean

Created Mathlib/Data/List/Permutation.lean

added theorem List.foldr_permutationsAux2

added theorem List.length_foldr_permutationsAux2'

added theorem List.length_foldr_permutationsAux2

added theorem List.length_permutationsAux2

added theorem List.map_map_permutations'Aux

added theorem List.map_map_permutationsAux2

added theorem List.map_permutations'

added theorem List.map_permutations

added theorem List.map_permutationsAux2'

added theorem List.map_permutationsAux2

added theorem List.map_permutationsAux

added theorem List.mem_foldr_permutationsAux2

added theorem List.mem_permutationsAux2'

added theorem List.mem_permutationsAux2

added theorem List.permutations'Aux_eq_permutationsAux2

added theorem List.permutationsAux2_append

added theorem List.permutationsAux2_comp_append

added theorem List.permutationsAux2_fst

added theorem List.permutationsAux2_snd_cons

added theorem List.permutationsAux2_snd_eq

added theorem List.permutationsAux_append

added theorem List.permutationsAux_cons

added theorem List.permutationsAux_nil

added theorem List.permutations_append

added theorem List.permutations_aux2_snd_nil

added theorem List.permutations_nil