Mathlib v3 is deprecated. Go to Mathlib v4

Theorem list.insert_nth_succ_nil

Modification history

2020-12-23 18:58

src/data/list/basic.lean

chore(order/filter/basic): make `filter.univ_mem_sets` a `simp` lemma (#5464)

Added list.insert_nth_succ_nil View on Github →