Zip

📁 Source: Mathlib/Data/Vector/Zip.lean

Statistics

Metric	Count
Definitions zipWith	1
Theorems prod_mul_prod_eq_prod_zipWith, sum_add_sum_eq_sum_zipWith, zipWith_get, zipWith_tail, zipWith_toList	5
Total	6

List.Vector

Definitions

Name	Category	Theorems
zipWith 📖	CompOp	5 math math: zipWith_get, zipWith_tail, zipWith_toList, sum_add_sum_eq_sum_zipWith, prod_mul_prod_eq_prod_zipWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_mul_prod_eq_prod_zipWith 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toOne toList zipWith	—	List.prod_mul_prod_eq_prod_zipWith_of_length_eq toList_length
sum_add_sum_eq_sum_zipWith 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toZero toList zipWith	—	List.sum_add_sum_eq_sum_zipWith_of_length_eq toList_length
zipWith_get 📖	mathematical	—	get zipWith	—	—
zipWith_tail 📖	mathematical	—	tail zipWith	—	ext get_tail zipWith_get
zipWith_toList 📖	mathematical	—	toList zipWith	—	—

---

← Back to Index