mathlib3

bc77a23e - feat(data/list/*): add left- and right-biased versions of map₂ and zip (#4512)

feat(data/list/*): add left- and right-biased versions of map₂ and zip (#4512) When given lists of different lengths, `map₂` and `zip` truncate the output to the length of the shorter input list. This commit adds variations on `map₂` and `zip` whose output is always as long as the left/right input.