Commit 2021-08-18 08:28 efa34dc6

View on Github →

feat(data/list/perm): nodup_permutations (#8616) A simpler version of #8494 TODO: nodup s.permutations ↔ nodup s TODO: count s s.permutations = (zip_with count s s.tails).prod

Estimated changes

Modified src/data/list/basic.lean

added theorem list.count_bind

added theorem list.count_map_map

added theorem list.inj_on_insert_nth_index_of_not_mem

added theorem list.insert_nth_injective

added theorem list.insert_nth_length_self

deleted theorem list.insert_nth_nil

added theorem list.insert_nth_of_length_lt

added theorem list.insert_nth_succ_cons

added theorem list.insert_nth_zero

added theorem list.length_insert_nth_le_succ

added theorem list.length_le_length_insert_nth

added theorem list.nth_le_insert_nth_add_succ

added theorem list.nth_le_insert_nth_of_lt

added theorem list.nth_le_insert_nth_self

Modified src/data/list/perm.lean

added theorem list.count_permutations'_aux_self

added theorem list.injective_permutations'_aux

added theorem list.length_permutations'_aux

added theorem list.nodup_permutations'_aux_iff

added theorem list.nodup_permutations'_aux_of_not_mem

added theorem list.nodup_permutations

added theorem list.nth_le_permutations'_aux

added theorem list.permutations'_aux_nth_le_zero