Mathlib v3 is deprecated. Go to Mathlib v4

Def vector.induction_on

Modification history

2021-09-20 08:13
src/data/vector/basic.lean
feat(data/vector/basic): induction principles (#9261)
Modified vector.induction_onView on Github →
2020-10-13 16:46
src/data/vector2.lean
feat(data/vector2): induction principle, define last, and some lemmas (blocked by #4578) (#4554)
Added vector.induction_onView on Github →