Def Vector.replicate

Modification history

2024-07-08 16:00

Mathlib/Data/Vector/Defs.lean

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

Deleted Vector.replicate View on Github →

2023-01-16 07:17

Mathlib/Data/Vector.lean

Refactor: drop `List.repeat` (#1579) …

Added Vector.replicate View on Github →