Commit 2024-03-21 05:04 bf26b9c5

View on Github →

chore: split insertNth lemmas from List.Basic (#11542) Removes the insertNth section of this long file to its own new file. This section seems to be completely independent of the rest of the file, so this is a fairly easy split to make.

Estimated changes

deleted theorem List.get_insertNth_of_lt
deleted theorem List.get_insertNth_self
deleted theorem List.insertNth_comm
deleted theorem List.insertNth_injective
deleted theorem List.insertNth_succ_cons
deleted theorem List.insertNth_succ_nil
deleted theorem List.insertNth_zero
deleted theorem List.length_insertNth
deleted theorem List.mem_insertNth
deleted theorem List.nthLe_insertNth_self
deleted theorem List.removeNth_insertNth
added theorem List.insertNth_comm
added theorem List.insertNth_zero
added theorem List.length_insertNth
added theorem List.mem_insertNth