Theorem Vector.get_tail

Modification history

2024-07-08 16:00

Mathlib/Data/Vector/Basic.lean

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

Deleted Vector.get_tail View on Github →

2024-05-27 07:37

Mathlib/Data/Vector/Basic.lean

chore: Do not import algebra in `Data.Vector` (#13242) …

Modified Vector.get_tail View on Github →

2023-01-19 10:14

Mathlib/Data/Vector/Basic.lean

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

Added Vector.get_tail View on Github →