Def Vector.nth

Modification history

2023-01-19 10:14

Mathlib/Data/Vector.lean

Feat: Port/data.vector.basic (#1633) …

Deleted Vector.nth View on Github →

2022-12-12 18:44

Mathlib/Data/Vector.lean

feat: port Data.Vector from lean-core (#834) …

Added Vector.nth View on Github →