Def Vector.drop

Modification history

2024-07-08 16:00

Mathlib/Data/Vector/Defs.lean

chore: Added namespace Mathlib around Vector defs (#13407) …

Deleted Vector.drop View on Github →

2022-12-12 18:44

Mathlib/Data/Vector.lean

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

Added Vector.drop View on Github →