Theorems · Theorem · combinatorics

List.Vector.toList_map

∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (v : List.Vector α n) (f : α → β),
  (List.Vector.map f v).toList = List.map f v.toList

Defined in

Mathlib.Data.Vector.Basic

Cited by

4 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext