Mathlib v3 is deprecated. Go to Mathlib v4

Def vector.{u}

Modification history

2018-10-17 22:49
data/vector2.lean
feature(data/vector2, data/list): add insert_nth for vectors and lists
Deleted vector.{u}View on Github →
2018-05-30 15:29
data/vector2.lean
feat(data/computablility): reduced partrec
Added vector.{u}View on Github →