Theorem Vector.inductionOn_cons

Modification history

2024-07-08 16:00

Mathlib/Data/Vector/Basic.lean

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

Deleted Vector.inductionOn_cons View on Github →

2024-06-08 02:35

Mathlib/Data/Vector/Basic.lean

feat: basic `Vector.inductionOn` API (#13616) …

Added Vector.inductionOn_cons View on Github →