Commit 2023-01-23 08:09 c4fa5bd4

View on Github →

feat: Port Data.Vector.Zip (#1705) Nothing complicated, just changing names

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Vector/Zip.lean

added theorem Vector.prod_mul_prod_eq_prod_zipWith

added def Vector.zipWith

added theorem Vector.zipWith_get

added theorem Vector.zipWith_tail

added theorem Vector.zipWith_toList