Commit 2022-11-24 15:26 3fcc5a49

View on Github →

refactor(data/list/sublists): move lemmas to remove as import (#17694) Material on sublists is not used until later, so can be concentrated into one file.

Estimated changes

Modified src/data/bitvec/core.lean

Modified src/data/list/nodup.lean

deleted theorem list.nodup_sublists'

deleted theorem list.nodup_sublists

deleted theorem list.nodup_sublists_len

Modified src/data/list/pairwise.lean

deleted theorem list.pairwise.sublists'

deleted theorem list.pairwise_sublists

Modified src/data/list/perm.lean

deleted theorem list.range_bind_sublists_len_perm

deleted theorem list.revzip_sublists'

deleted theorem list.revzip_sublists

deleted theorem list.sublists_cons_perm_append

deleted theorem list.sublists_perm_sublists'

Modified src/data/list/sublists.lean

added theorem list.nodup_sublists'

added theorem list.nodup_sublists

added theorem list.nodup_sublists_len

added theorem list.pairwise.sublists'

added theorem list.pairwise_sublists

added theorem list.range_bind_sublists_len_perm

added theorem list.revzip_sublists'

added theorem list.revzip_sublists

added theorem list.sublists_cons_perm_append

added theorem list.sublists_perm_sublists'

Modified src/data/multiset/powerset.lean