Mathlib v3 is deprecated. Go to Mathlib v4

Theorem list.eq_nil_of_forall_not_mem

Modification history

2019-03-09 17:49

src/data/list/basic.lean

refactor(data/list): rm redundant eq_nil_of_forall_not_mem (#804)

Deleted list.eq_nil_of_forall_not_mem View on Github →

2017-07-24 00:42

data/list/basic.lean

refactor(*): move in some nat lemmas …

Added list.eq_nil_of_forall_not_mem View on Github →