zip): remove a hypothesis from `map_fst_zip` and `map_snd_zip`

Commit

3 years ago

feat(data/list/zip): remove a hypothesis from `map_fst_zip` and `map_snd_zip` There is still something interesting to say here if the lists are not the same length.

References

eric-wieser/list.zip-lemmas

Author

eric-wieser

Parents

23f67f2f

mathlib 3b7fa0d3 - feat(data/list/zip): remove a hypothesis from `map_fst_zip` and `map_snd_zip`

mathlib
3b7fa0d3 - feat(data/list/zip): remove a hypothesis from `map_fst_zip` and `map_snd_zip`