Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-03 07:18 2a9ad03c

View on Github →

feat(data/list/basic): more lemmas about list.chain'; chain'_of_pairwise → pairwise.chain' (#2071)

Estimated changes

added theorem list.chain'.cons
added theorem list.chain'.tail
added theorem list.chain'_cons
added theorem list.chain'_nil
deleted theorem list.chain'_of_pairwise
added theorem list.chain'_pair
added theorem list.chain'_reverse
modified theorem list.chain'_singleton
added theorem list.chain.imp'
added theorem list.pairwise.chain'