Commit 2023-01-05 15:50 f4cd7f1e

View on Github →

feat: Port Data.List.Lemmas (#1351)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Lemmas.lean

added theorem List.injOn_insertNth_index_of_not_mem

added theorem List.range_map

added theorem List.range_map_coe