Commit 2023-06-27 13:14 cda66a7b

View on Github →

feat: Add simp lemmas for vectors, and a way to index vectors with Nats (#4994) Co-authored-by Chris Hughes

Estimated changes

Modified Mathlib/Data/Vector.lean

Modified Mathlib/Data/Vector/Basic.lean

added theorem Vector.append_nil

added def Vector.casesOn

added def Vector.casesOn₂

added def Vector.casesOn₃

added theorem Vector.get_append_cons_succ

added theorem Vector.get_append_cons_zero

added theorem Vector.get_map₂

added theorem Vector.map₂_cons

added theorem Vector.map₂_nil

added theorem Vector.replicate_succ