Def Vector.casesOn

Modification history

2024-07-08 16:00

Mathlib/Data/Vector/Basic.lean

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

Deleted Vector.casesOn View on Github →

2023-08-10 19:52

Mathlib/Data/Vector/Basic.lean

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

Modified Vector.casesOn View on Github →

2023-06-27 13:14

Mathlib/Data/Vector/Basic.lean

feat: Add simp lemmas for vectors, and a way to index vectors with Nats (#4994) …

Added Vector.casesOn View on Github →