Def Vector.inductionOn

Modification history

2024-07-08 16:00

Mathlib/Data/Vector/Basic.lean

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

Deleted Vector.inductionOn View on Github →

2023-08-10 19:52

Mathlib/Data/Vector/Basic.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Vector.inductionOn View on Github →

2023-01-20 17:48

Mathlib/Data/Vector/Basic.lean

fix: make List.rec and Nat.rec computable (#1720) …

Added Vector.inductionOn View on Github →