Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-20 08:13 d93c6a85

View on Github →

feat(data/vector/basic): induction principles (#9261)

Estimated changes

Modified src/data/vector/basic.lean

modified def vector.induction_on

added def vector.induction_on₂

added def vector.induction_on₃