Commit 2023-01-10 08:27 4f6d3be3

View on Github →

feat: port Data.List.Zip (#1416)

depends on: #1380

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Zip.lean

added theorem List.all₂_zipWith

added theorem List.get?_zip_eq_some

added theorem List.get?_zip_with

added theorem List.get?_zip_with_eq_some

added theorem List.get_zip

added theorem List.get_zipWith

added theorem List.length_revzip

added theorem List.length_zip

added theorem List.lt_length_left_of_zip

added theorem List.lt_length_left_of_zipWith

added theorem List.lt_length_right_of_zip

added theorem List.lt_length_right_of_zipWith

added theorem List.map_fst_zip

added theorem List.map_prod_left_eq_zip

added theorem List.map_prod_right_eq_zip

added theorem List.map_snd_zip

added theorem List.map_uncurry_zip_eq_zipWith

added theorem List.map_zipWith

added theorem List.mem_zip

added theorem List.mem_zip_inits_tails

added theorem List.nthLe_zip

added theorem List.nthLe_zipWith

added theorem List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop

added theorem List.prod_mul_prod_eq_prod_zipWith_of_length_eq

added theorem List.reverse_revzip

added theorem List.revzip_map_fst

added theorem List.revzip_map_snd

added theorem List.revzip_swap

added theorem List.sum_zipWith_distrib_left

added theorem List.unzip_cons

added theorem List.unzip_eq_map

added theorem List.unzip_left

added theorem List.unzip_nil

added theorem List.unzip_revzip

added theorem List.unzip_right

added theorem List.unzip_swap

added theorem List.unzip_zip

added theorem List.unzip_zip_left

added theorem List.unzip_zip_right

added theorem List.zipWith3_same_left

added theorem List.zipWith3_same_mid

added theorem List.zipWith3_same_right

added theorem List.zipWith_append

added theorem List.zipWith_comm

added theorem List.zipWith_comm_of_comm

added theorem List.zipWith_congr

added theorem List.zipWith_cons_cons

added theorem List.zipWith_distrib_drop

added theorem List.zipWith_distrib_reverse

added theorem List.zipWith_distrib_tail

added theorem List.zipWith_distrib_take

added theorem List.zipWith_eq_nil_iff

added theorem List.zipWith_map

added theorem List.zipWith_map_left

added theorem List.zipWith_map_right

added theorem List.zipWith_nil_left

added theorem List.zipWith_nil_right

added theorem List.zipWith_same

added theorem List.zipWith_zipWith_left

added theorem List.zipWith_zipWith_right

added theorem List.zip_append

added theorem List.zip_cons_cons

added theorem List.zip_map'

added theorem List.zip_map

added theorem List.zip_map_left

added theorem List.zip_map_right

added theorem List.zip_nil_left

added theorem List.zip_nil_right

added theorem List.zip_of_prod

added theorem List.zip_swap

added theorem List.zip_unzip