Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-17 11:35 b7d74c43

View on Github →

feat(data/list): list.chain' for empty chains

Estimated changes

Modified data/list/basic.lean

added theorem list.chain'.iff

added theorem list.chain'.iff_mem

added theorem list.chain'.imp

added theorem list.chain'_iff_pairwise

added theorem list.chain'_map

added theorem list.chain'_map_of_chain'

added theorem list.chain'_of_chain'_map

added theorem list.chain'_of_pairwise

added theorem list.chain'_singleton

added theorem list.chain'_split

modified theorem list.chain.iff_mem

modified theorem list.nodup_nil

Modified data/list/defs.lean

added def list.chain'

Modified data/list/sort.lean

modified theorem list.sorted_nil

Modified data/multiset.lean

modified theorem multiset.nodup_zero