revzip of a mapped list #
List.revzip_map: revzip commutes with map, componentwise, the map companion of
List.revzip_map_fst and List.revzip_map_snd and the revzip instance of List.zip_map.
[UPSTREAM] candidate for Mathlib/Data/List/Zip.lean.
@[simp]
theorem
List.revzip_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(l : List α)
:
(map f l).revzip = map (Prod.map f f) l.revzip