Commit 2024-11-03 19:16 bfe53a05

View on Github →

feat(Data/Vector): add pmap for vectors and prove some lemmas (#17189)

Estimated changes

Modified Mathlib/Data/Vector/Basic.lean

added theorem Mathlib.Vector.getElem_map

added theorem Mathlib.Vector.getElem_pmap

added theorem Mathlib.Vector.head_pmap

added theorem Mathlib.Vector.pmap_cons'

added theorem Mathlib.Vector.pmap_cons

added theorem Mathlib.Vector.tail_pmap

added theorem Mathlib.Vector.toList_pmap

Modified Mathlib/Data/Vector/Defs.lean

added theorem Mathlib.Vector.getElem_def

added def Mathlib.Vector.pmap

added theorem Mathlib.Vector.pmap_nil

added theorem Mathlib.Vector.toList_getElem

Modified Mathlib/Data/Vector/MapLemmas.lean

added theorem Mathlib.Vector.map_pmap

added theorem Mathlib.Vector.pmap_map