Commit 2024-04-27 19:40 44a14fbb

View on Github →

chore(Data/Set/List): nthLe -> get migration (#12398)

Estimated changes

Modified Mathlib/Data/Set/List.lean

added theorem Set.range_list_get

deleted theorem Set.range_list_nthLe