pairwise): add `list.pairwise_pmap` and `list.pairwise.pmap` (#5273)

Commit

5 years ago

chore(data/list/pairwise): add `list.pairwise_pmap` and `list.pairwise.pmap` (#5273) Also add `list.pairwise.tail` and use it in the proof of `list.sorted.tail`.

Author

urkud

Parents

3f4829cd

mathlib 8f42d73d - chore(data/list/pairwise): add `list.pairwise_pmap` and `list.pairwise.pmap` (#5273)

mathlib
8f42d73d - chore(data/list/pairwise): add `list.pairwise_pmap` and `list.pairwise.pmap` (#5273)