Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-13 16:46 7cff8250

View on Github →

feat(data/vector2): induction principle, define last, and some lemmas (blocked by #4578) (#4554)

Estimated changes

Modified src/data/vector2.lean

added def vector.induction_on

added def vector.last

added theorem vector.last_def

added theorem vector.nth_cons_nil

added theorem vector.reverse_nth_zero

added theorem vector.singleton_tail

added theorem vector.tail_nil

added theorem vector.to_list_reverse

added theorem vector.to_list_singleton