Def Vector.eraseIdx

Modification history

2024-07-08 16:00

Mathlib/Data/Vector/Defs.lean

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

Deleted Vector.eraseIdx View on Github →

2024-05-06 07:35

Mathlib/Data/Vector.lean

chore: migrate from `List.removeNth` to `List.eraseIdx` (#12660)

Added Vector.eraseIdx View on Github →