Zip
📁 Source: Mathlib/Data/List/Zip.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
Theoremsforall_zipWith, instIsSymmOpZipWith, length_revzip, mem_zip_inits_tails, reverse_revzip, revzip_map_fst, revzip_map_snd, revzip_swap, rightInverse_unzip_zip, unzip_revzip, unzip_swap, zipWith3_same_left, zipWith3_same_mid, zipWith3_same_right, zipWith_congr, zipWith_zipWith_left, zipWith_zipWith_right, zip_swap | 18 |
| Total | 18 |
List
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
forall_zipWith 📖 | mathematical | — | Forall | — | — |
instIsSymmOpZipWith 📖 | mathematical | — | IsSymmOp | — | IsSymmOp.symm_op |
length_revzip 📖 | — | — | — | — | min_self |
mem_zip_inits_tails 📖 | — | — | — | — | — |
reverse_revzip 📖 | — | — | — | — | — |
revzip_map_fst 📖 | — | — | — | — | unzip_revzip |
revzip_map_snd 📖 | — | — | — | — | unzip_revzip |
revzip_swap 📖 | — | — | — | — | zip_swap |
rightInverse_unzip_zip 📖 | — | — | — | — | — |
unzip_revzip 📖 | — | — | — | — | — |
unzip_swap 📖 | — | — | — | — | — |
zipWith3_same_left 📖 | mathematical | — | zipWith3 | — | — |
zipWith3_same_mid 📖 | mathematical | — | zipWith3 | — | — |
zipWith3_same_right 📖 | mathematical | — | zipWith3 | — | — |
zipWith_congr 📖 | — | — | — | — | — |
zipWith_zipWith_left 📖 | mathematical | — | zipWith3 | — | — |
zipWith_zipWith_right 📖 | mathematical | — | zipWith3 | — | — |
zip_swap 📖 | — | — | — | — | — |
---