theorem Vector.toArray_injective {α : Type u_1} {n : Nat} {v w : Vector α n} : v.toArray = w.toArray → v = w

mk lemmas

@[simp]

theorem Vector.get_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Fin n) : (mk a h).get i = a[i]

@[simp]

theorem Vector.getD_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : Nat) (x : α) : (mk a h).getD i x = a.getD i x

@[simp]

theorem Vector.uget_mk {α : Type u_1} {n : Nat} (a : Array α) (h : a.size = n) (i : USize) (hi : i.toNat < n) : (mk a h).uget i hi = a.uget i ⋯

tail lemmas

theorem Vector.tail_eq_of_zero {α : Type u_1} {v : Vector α 0} : v.tail = #v[]

theorem Vector.tail_eq_of_ne_zero {n : Nat} {α : Type u_1} [NeZero n] {v : Vector α n} : v.tail = v.eraseIdx 0 ⋯

theorem Vector.toList_tail {α : Type u_1} {n : Nat} {v : Vector α n} : v.tail.toList = v.toList.tail

getElem lemmas

theorem Vector.getElem_tail {α : Type u_1} {n : Nat} {v : Vector α n} {i : Nat} (hi : i < n - 1) : v.tail[i] = v[i + 1]

get lemmas

theorem Vector.get_eq_getElem {α : Type u_1} {n : Nat} (v : Vector α n) (i : Fin n) : v.get i = v[↑i]

@[simp]

theorem Vector.get_push_last {α : Type u_1} {n : Nat} (v : Vector α n) (a : α) : (v.push a).get (Fin.last n) = a

@[simp]

theorem Vector.get_push_castSucc {α : Type u_1} {n : Nat} (v : Vector α n) (a : α) (i : Fin n) : (v.push a).get i.castSucc = v.get i

@[simp]

theorem Vector.get_map {α : Type u_1} {n : Nat} {β : Type u_2} (v : Vector α n) (f : α → β) (i : Fin n) : (map f v).get i = f (v.get i)

@[simp]

theorem Vector.get_reverse {α : Type u_1} {n : Nat} (v : Vector α n) (i : Fin n) : v.reverse.get i = v.get i.rev

@[simp]

theorem Vector.get_replicate {α : Type u_1} (n : Nat) (a : α) (i : Fin n) : (replicate n a).get i = a

@[simp]

theorem Vector.get_range (n : Nat) (i : Fin n) : (range n).get i = ↑i

@[simp]

theorem Vector.get_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Fin n) : (ofFn f).get i = f i

@[simp]

theorem Vector.get_cast {α : Type u_1} {m n : Nat} (v : Vector α m) (h : m = n) (i : Fin n) : (Vector.cast h v).get i = v.get (Fin.cast ⋯ i)

theorem Vector.get_tail {α : Type u_1} {n : Nat} (v : Vector α (n + 1)) (i : Fin n) : v.tail.get i = v.get i.succ

finIdxOf? lemmas

@[simp]

theorem Vector.finIdxOf?_empty {α : Type u_1} {a : α} [BEq α] (v : Vector α 0) : v.finIdxOf? a = none

@[simp]

theorem Vector.finIdxOf?_eq_none_iff {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {v : Vector α n} {a : α} : v.finIdxOf? a = none ↔ ¬a ∈ v

@[simp]

theorem Vector.finIdxOf?_eq_some_iff {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] {v : Vector α n} {a : α} {i : Fin n} : v.finIdxOf? a = some i ↔ v.get i = a ∧ ∀ (j : Fin n), j < i → ¬v.get j = a

@[simp]

theorem Vector.isSome_finIdxOf? {α : Type u_1} {n : Nat} [BEq α] [PartialEquivBEq α] {v : Vector α n} {a : α} : (v.finIdxOf? a).isSome = v.contains a

@[simp]

theorem Vector.isNone_finIdxOf? {α : Type u_1} {n : Nat} [BEq α] [PartialEquivBEq α] {v : Vector α n} {a : α} : (v.finIdxOf? a).isNone = !v.contains a

theorem Vector.toArray_scanlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Vector α n} : toArray <$> scanlM f init as = Array.scanlM f init as.toArray

theorem Vector.toArray_scanrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Vector α n} : toArray <$> scanrM f init as = Array.scanrM f init as.toArray

scanlM/scanrM lemmas

@[simp]

theorem Vector.toList_scanlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Vector α n} : toList <$> scanlM f init as = List.scanlM f init as.toList

@[simp]

theorem Vector.toList_scanrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : α → β → m β} {as : Vector α n} : toList <$> scanrM f init as = List.scanrM f init as.toList

@[simp]

theorem Vector.scanlM_empty {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} : scanlM f init #v[] = pure #v[init]

@[simp]

theorem Vector.scanrM_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] {f : α → β → m β} : scanrM f init #v[] = pure #v[init]

theorem Vector.scanlM_reverse {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : β → α → m β} {as : Vector α n} : scanlM f init as.reverse = reverse <$> scanrM (flip f) init as

@[simp]

theorem Vector.scanlM_pure {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : β → α → β} {as : Vector α n} : scanlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init as = pure (scanl f init as)

@[simp]

theorem Vector.scanrM_pure {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : α → β → β} {as : Vector α n} : scanrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) init as = pure (scanr f init as)

theorem Vector.idRun_scanlM {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → Id β} {as : Vector α n} : (scanlM f init as).run = scanl (fun (x1 : β) (x2 : α) => (f x1 x2).run) init as

theorem Vector.idRun_scanrM {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → Id β} {as : Vector α n} : (scanrM f init as).run = scanr (fun (x1 : α) (x2 : β) => (f x1 x2).run) init as

theorem Vector.scanlM_map {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : α₁ → α₂} {g : β → α₂ → m β} {as : Vector α₁ n} : scanlM g init (map f as) = scanlM (fun (x1 : β) (x2 : α₁) => g x1 (f x2)) init as

theorem Vector.scanrM_map {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {n : Nat} {init : β} [Monad m] [LawfulMonad m] {f : α₁ → α₂} {g : α₂ → β → m β} {as : Vector α₁ n} : scanrM g init (map f as) = scanrM (fun (a : α₁) (b : β) => g (f a) b) init as

scanl/scanr lemmas

theorem Vector.scanl_eq_scanlM {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} : scanl f init as = (scanlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init as).run

theorem Vector.scanr_eq_scanrM {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} : scanr f init as = (scanrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) init as).run

theorem Vector.toArray_scanl {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} : (scanl f init as).toArray = Array.scanl f init as.toArray

theorem Vector.toArray_scanr {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} : (scanr f init as).toArray = Array.scanr f init as.toArray

@[simp]

theorem Vector.toList_scanl {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} : (scanl f init as).toList = List.scanl f init as.toList

@[simp]

theorem Vector.toList_scanr {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} : (scanr f init as).toList = List.scanr f init as.toList

theorem Vector.scanl_empty {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} : scanl f init #v[] = #v[init]

theorem Vector.scanr_empty {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} : scanr f init #v[] = #v[init]

theorem Vector.scanl_singleton {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {a : α} : scanl f init #v[a] = #v[init, f init a]

@[simp]

theorem Vector.getElem_scanl {β : Type u_1} {α : Type u_2} {n i : Nat} {init : β} {f : β → α → β} {as : Vector α n} (h : i < n + 1) : (scanl f init as)[i] = foldl f init (as.take i)

@[simp]

theorem Vector.getElem_scanr {α : Type u_1} {β : Type u_2} {n i : Nat} {init : β} {f : α → β → β} {as : Vector α n} (h : i < n + 1) : (scanr f init as)[i] = foldr f init (as.drop i)

theorem Vector.getElem?_scanl {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {i : Nat} {f : β → α → β} {as : Vector α n} : (scanl f init as)[i]? = if i ≤ n then some (foldl f init (as.take i)) else none

theorem Vector.getElem?_scanr {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {i : Nat} {f : α → β → β} {as : Vector α n} : (scanr f init as)[i]? = if i < n + 1 then some (foldr f init (as.drop i)) else none

theorem Vector.getElem_scanl_zero {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} : (scanl f init as)[0] = init

theorem Vector.getElem_scanr_zero {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} : (scanr f init as)[0] = foldr f init as

theorem Vector.getElem?_scanl_zero {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} : (scanl f init as)[0]? = some init

theorem Vector.getElem?_scanr_zero {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} : (scanr f init as)[0]? = some (foldr f init as)

theorem Vector.getElem?_succ_scanl {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {i : Nat} {f : β → α → β} {as : Vector α n} : (scanl f init as)[i + 1]? = (scanl f init as)[i]?.bind fun (x : β) => Option.map (fun (y : α) => f x y) as[i]?

theorem Vector.getElem_succ_scanl {β : Type u_1} {α : Type u_2} {n i : Nat} {init : β} {f : β → α → β} {as : Vector α n} (h : i + 1 < n + 1) : (scanl f init as)[i + 1] = f (scanl f init as)[i] as[i]

theorem Vector.scanl_push {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} {a : α} : scanl f init (as.push a) = (scanl f init as).push (f (foldl f init as) a)

theorem Vector.scanr_push {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} {a : α} : scanr f init (as.push a) = (scanr f (f a init) as).push init

theorem Vector.scanl_map {γ : Type u_1} {β : Type u_2} {α : Type u_3} {n : Nat} {init : γ} {f : γ → β → γ} {g : α → β} {as : Vector α n} : scanl f init (map g as) = scanl (fun (x1 : γ) (x2 : α) => f x1 (g x2)) init as

theorem Vector.scanr_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : Nat} {init : γ} {f : β → γ → γ} {g : α → β} {as : Vector α n} : scanr f init (map g as) = scanr (fun (x : α) (acc : γ) => f (g x) acc) init as

theorem Vector.scanl_reverse {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} : scanl f init as.reverse = (scanr (flip f) init as).reverse

theorem Vector.scanr_reverse {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} : scanr f init as.reverse = (scanl (flip f) init as).reverse

@[simp]

theorem Vector.back_scanl {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} : (scanl f init as).back = foldl f init as

@[simp]

theorem Vector.back_scanr {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} : (scanr f init as).back = init

theorem Vector.back?_scanl {β : Type u_1} {α : Type u_2} {n : Nat} {init : β} {f : β → α → β} {as : Vector α n} : (scanl f init as).back? = some (foldl f init as)

theorem Vector.back?_scanr {α : Type u_1} {β : Type u_2} {n : Nat} {init : β} {f : α → β → β} {as : Vector α n} : (scanr f init as).back? = some init