Commit 2023-03-31 14:20 dcbcc203

View on Github →

feat: port Data.Set.List + leanprover-community/mathlib#18647 (#3203)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Lemmas.lean

deleted theorem List.range_map

deleted theorem List.range_map_coe

Modified Mathlib/Data/Multiset/Basic.lean

Created Mathlib/Data/Set/List.lean

added theorem Set.range_list_get?

added theorem Set.range_list_getD

added theorem Set.range_list_getI

added theorem Set.range_list_map

added theorem Set.range_list_map_coe

added theorem Set.range_list_nthLe

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

Modified test/lift.lean