Commit 2023-07-10 11:07 507d89c1

View on Github →

feat: simplification lemmas for Vector.map / Vector.mapAccumr (#5558) Primarily focused on folding nested applications of mapAccumr into a single mapAccumr

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Vector/Basic.lean

Created Mathlib/Data/Vector/MapLemmas.lean

added theorem Vector.mapAccumr_bisim

added theorem Vector.mapAccumr_bisim_tail

added theorem Vector.mapAccumr_eq_map

added theorem Vector.mapAccumr_eq_map_of_constant_state

added theorem Vector.mapAccumr_eq_map_of_unused_state

added theorem Vector.mapAccumr_map

added theorem Vector.mapAccumr_mapAccumr

added theorem Vector.mapAccumr_mapAccumr₂

added theorem Vector.mapAccumr_redundant_pair

added theorem Vector.mapAccumr₂_bisim

added theorem Vector.mapAccumr₂_bisim_tail

added theorem Vector.mapAccumr₂_comm

added theorem Vector.mapAccumr₂_eq_map₂

added theorem Vector.mapAccumr₂_eq_map₂_of_constant_state

added theorem Vector.mapAccumr₂_eq_map₂_of_unused_state

added theorem Vector.mapAccumr₂_flip

added theorem Vector.mapAccumr₂_mapAccumr_left

added theorem Vector.mapAccumr₂_mapAccumr_right

added theorem Vector.mapAccumr₂_mapAccumr₂_left_left

added theorem Vector.mapAccumr₂_mapAccumr₂_left_right

added theorem Vector.mapAccumr₂_mapAccumr₂_right_left

added theorem Vector.mapAccumr₂_mapAccumr₂_right_right

added theorem Vector.mapAccumr₂_redundant_pair

added theorem Vector.mapAccumr₂_unused_input_left

added theorem Vector.mapAccumr₂_unused_input_right

added theorem Vector.map_map

added theorem Vector.map_mapAccumr

added theorem Vector.map_map₂

added theorem Vector.map₂_comm

added theorem Vector.map₂_flip

added theorem Vector.map₂_map_left

added theorem Vector.map₂_map_right

Modified Mathlib/Data/Vector/Snoc.lean