Commit 2023-03-30 03:40 2ec920d3

View on Github →

feat(data/list/lemmas): add lemmas about set.range list.nth* (#18647) Add versions for list.nth_le, list.nth, list.nthd, and list.inth. Also move lemmas from list to set namespace.

Estimated changes

Modified src/data/list/lemmas.lean

deleted theorem list.range_map

deleted theorem list.range_map_coe

Modified src/data/multiset/basic.lean

Created src/data/set/list.lean

added theorem set.range_list_inth

added theorem set.range_list_map

added theorem set.range_list_map_coe

added theorem set.range_list_nth

added theorem set.range_list_nth_le

added theorem set.range_list_nthd

Modified src/group_theory/submonoid/membership.lean