Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.vector_equiv_array

Modification history

2023-01-19 15:23
src/data/array/lemmas.lean
chore(data/fintype/vector, logic/equiv/list): split (#18226) …
Modified equiv.vector_equiv_arrayView on Github →
2018-07-30 11:48
data/array/lemmas.lean
feat(category/traversable): instances for various collections (#217)
Modified equiv.vector_equiv_arrayView on Github →
2018-06-30 23:04
data/equiv/basic.lean
refactor(data/equiv): reorganize data.equiv deps
Modified equiv.vector_equiv_arrayView on Github →
2018-05-29 17:20
data/equiv.lean
feat(computability/primrec): add traditional primrec definition …
Added equiv.vector_equiv_arrayView on Github →