Additional theorems and definitions about the Vector type

This file introduces the infix notation ::ᵥ for Vector.cons.

def List.Vector.«term_::ᵥ_» : Lean.TrailingParserDescr

If a : α and l : Vector α n, then cons a l, is the vector of length n + 1 whose first element is a and with l as the rest of the list.

Equations

• List.Vector.«term_::ᵥ_» = Lean.ParserDescr.trailingNode `List.Vector.«term_::ᵥ_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ᵥ ") (Lean.ParserDescr.cat `term 67))

instance List.Vector.instInhabited {α : Type u_1} {n : ℕ} [Inhabited α] : Inhabited (Vector α n)

Equations

• List.Vector.instInhabited = { default := List.Vector.ofFn default }

theorem List.Vector.toList_injective {α : Type u_1} {n : ℕ} : Function.Injective toList

theorem List.Vector.ext {α : Type u_1} {n : ℕ} {v w : Vector α n} : (∀ (m : Fin n), v.get m = w.get m) → v = w

Two v w : Vector α n are equal iff they are equal at every single index.

theorem List.Vector.ext_iff {α : Type u_1} {n : ℕ} {v w : Vector α n} : v = w ↔ ∀ (m : Fin n), v.get m = w.get m

instance List.Vector.zero_subsingleton {α : Type u_1} : Subsingleton (Vector α 0)

The empty Vector is a Subsingleton.

@[simp]

theorem List.Vector.cons_val {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) : ↑(a ::ᵥ v) = a :: ↑v

theorem List.Vector.eq_cons_iff {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n.succ) (v' : Vector α n) : v = a ::ᵥ v' ↔ v.head = a ∧ v.tail = v'

theorem List.Vector.ne_cons_iff {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n.succ) (v' : Vector α n) : v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'

theorem List.Vector.exists_eq_cons {α : Type u_1} {n : ℕ} (v : Vector α n.succ) : ∃ (a : α) (as : Vector α n), v = a ::ᵥ as

@[simp]

theorem List.Vector.toList_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) : (ofFn f).toList = List.ofFn f

@[simp]

theorem List.Vector.mk_toList {α : Type u_1} {n : ℕ} (v : Vector α n) (h : v.toList.length = n) : ⟨v.toList, h⟩ = v

@[simp]

theorem List.Vector.length_val {α : Type u_1} {n : ℕ} (v : Vector α n) : (↑v).length = n

@[simp]

theorem List.Vector.pmap_cons {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n) (hp : ∀ x ∈ (a ::ᵥ v).toList, p x) : pmap f (a ::ᵥ v) hp = f a ⋯ ::ᵥ pmap f v ⋯

theorem List.Vector.pmap_cons' {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n) (ha : p a) (hp : ∀ x ∈ v.toList, p x) : f a ha ::ᵥ pmap f v hp = pmap f (a ::ᵥ v) ⋯

Opposite direction of Vector.pmap_cons

@[simp]

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

@[simp]

theorem List.Vector.head_map {α : Type u_1} {n : ℕ} {β : Type u_6} (v : Vector α (n + 1)) (f : α → β) : (map f v).head = f v.head

@[simp]

theorem List.Vector.tail_map {α : Type u_1} {n : ℕ} {β : Type u_6} (v : Vector α (n + 1)) (f : α → β) : (map f v).tail = map f v.tail

@[simp]

theorem List.Vector.getElem_map {α : Type u_1} {n : ℕ} {β : Type u_6} (v : Vector α n) (f : α → β) {i : ℕ} (hi : i < n) : (map f v)[i] = f v[i]

@[simp]

theorem List.Vector.toList_pmap {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n) (hp : ∀ x ∈ v.toList, p x) : (pmap f v hp).toList = List.pmap f v.toList hp

@[simp]

theorem List.Vector.head_pmap {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1)) (hp : ∀ x ∈ v.toList, p x) : (pmap f v hp).head = f v.head ⋯

@[simp]

theorem List.Vector.tail_pmap {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1)) (hp : ∀ x ∈ v.toList, p x) : (pmap f v hp).tail = pmap f v.tail ⋯

@[simp]

theorem List.Vector.getElem_pmap {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n) (hp : ∀ x ∈ v.toList, p x) {i : ℕ} (hi : i < n) : (pmap f v hp)[i] = f v[i] ⋯

theorem List.Vector.get_eq_get_toList {α : Type u_1} {n : ℕ} (v : Vector α n) (i : Fin n) : v.get i = v.toList.get (Fin.cast ⋯ i)

@[deprecated List.Vector.get_eq_get_toList (since := "2024-12-20")]

theorem List.Vector.get_eq_get {α : Type u_1} {n : ℕ} (v : Vector α n) (i : Fin n) : v.get i = v.toList.get (Fin.cast ⋯ i)

Alias of List.Vector.get_eq_get_toList.

@[simp]

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

@[simp]

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

@[simp]

theorem List.Vector.map₂_nil {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) : map₂ f nil nil = nil

@[simp]

theorem List.Vector.map₂_cons {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (hd₁ : α) (tl₁ : Vector α n) (hd₂ : β) (tl₂ : Vector β n) (f : α → β → γ) : map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ map₂ f tl₁ tl₂

@[simp]

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

@[simp]

theorem List.Vector.ofFn_get {α : Type u_1} {n : ℕ} (v : Vector α n) : ofFn v.get = v

def Equiv.vectorEquivFin (α : Type u_6) (n : ℕ) : List.Vector α n ≃ (Fin n → α)

The natural equivalence between length-n vectors and functions from Fin n.

Equations

• Equiv.vectorEquivFin α n = { toFun := List.Vector.get, invFun := List.Vector.ofFn, left_inv := ⋯, right_inv := ⋯ }

theorem List.Vector.get_tail {α : Type u_1} {n : ℕ} (x : Vector α n) (i : Fin (n - 1)) : x.tail.get i = x.get ⟨↑i + 1, ⋯⟩

@[simp]

theorem List.Vector.get_tail_succ {α : Type u_1} {n : ℕ} (v : Vector α n.succ) (i : Fin n) : v.tail.get i = v.get i.succ

@[simp]

theorem List.Vector.tail_val {α : Type u_1} {n : ℕ} (v : Vector α n.succ) : ↑v.tail = (↑v).tail

@[simp]

theorem List.Vector.tail_nil {α : Type u_1} : nil.tail = nil

The tail of a nil vector is nil.

@[simp]

theorem List.Vector.singleton_tail {α : Type u_1} (v : Vector α 1) : v.tail = nil

The tail of a vector made up of one element is nil.

@[simp]

theorem List.Vector.tail_ofFn {α : Type u_1} {n : ℕ} (f : Fin n.succ → α) : (ofFn f).tail = ofFn fun (i : Fin n) => f i.succ

@[simp]

theorem List.Vector.toList_empty {α : Type u_1} (v : Vector α 0) : v.toList = []

@[simp]

theorem List.Vector.toList_singleton {α : Type u_1} (v : Vector α 1) : v.toList = [v.head]

The list that makes up a Vector made up of a single element, retrieved via toList, is equal to the list of that single element.

@[simp]

theorem List.Vector.empty_toList_eq_ff {α : Type u_1} {n : ℕ} (v : Vector α (n + 1)) : v.toList.isEmpty = false

theorem List.Vector.not_empty_toList {α : Type u_1} {n : ℕ} (v : Vector α (n + 1)) : ¬v.toList.isEmpty = true

@[simp]

theorem List.Vector.map_id {α : Type u_1} {n : ℕ} (v : Vector α n) : map id v = v

Mapping under id does not change a vector.

theorem List.Vector.nodup_iff_injective_get {α : Type u_1} {n : ℕ} {v : Vector α n} : v.toList.Nodup ↔ Function.Injective v.get

theorem List.Vector.head?_toList {α : Type u_1} {n : ℕ} (v : Vector α n.succ) : v.toList.head? = some v.head

def List.Vector.reverse {α : Type u_1} {n : ℕ} (v : Vector α n) : Vector α n

Reverse a vector.

Equations

• v.reverse = ⟨v.toList.reverse, ⋯⟩

theorem List.Vector.toList_reverse {α : Type u_1} {n : ℕ} {v : Vector α n} : v.reverse.toList = v.toList.reverse

The List of a vector after a reverse, retrieved by toList is equal to the List.reverse after retrieving a vector's toList.

@[simp]

theorem List.Vector.reverse_reverse {α : Type u_1} {n : ℕ} {v : Vector α n} : v.reverse.reverse = v

@[simp]

theorem List.Vector.get_zero {α : Type u_1} {n : ℕ} (v : Vector α n.succ) : v.get 0 = v.head

@[simp]

theorem List.Vector.head_ofFn {α : Type u_1} {n : ℕ} (f : Fin n.succ → α) : (ofFn f).head = f 0

theorem List.Vector.get_cons_zero {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) : (a ::ᵥ v).get 0 = a

@[simp]

theorem List.Vector.get_cons_nil {α : Type u_1} {ix : Fin 1} (x : α) : (x ::ᵥ nil).get ix = x

Accessing the nth element of a vector made up of one element x : α is x itself.

@[simp]

theorem List.Vector.get_cons_succ {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) (i : Fin n) : (a ::ᵥ v).get i.succ = v.get i

def List.Vector.last {α : Type u_1} {n : ℕ} (v : Vector α (n + 1)) : α

The last element of a Vector, given that the vector is at least one element.

Equations

• v.last = v.get (Fin.last n)

theorem List.Vector.last_def {α : Type u_1} {n : ℕ} {v : Vector α (n + 1)} : v.last = v.get (Fin.last n)

The last element of a Vector, given that the vector is at least one element.

theorem List.Vector.reverse_get_zero {α : Type u_1} {n : ℕ} {v : Vector α (n + 1)} : v.reverse.head = v.last

The last element of a vector is the head of the reverse vector.

def List.Vector.scanl {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : Vector α n) : Vector β (n + 1)

Construct a Vector β (n + 1) from a Vector α n by scanning f : β → α → β from the "left", that is, from 0 to Fin.last n, using b : β as the starting value.

Equations

• List.Vector.scanl f b v = ⟨List.scanl f b v.toList, ⋯⟩

@[simp]

theorem List.Vector.scanl_nil {α : Type u_1} {β : Type u_6} (f : β → α → β) (b : β) : scanl f b nil = b ::ᵥ nil

Providing an empty vector to scanl gives the starting value b : β.

@[simp]

theorem List.Vector.scanl_cons {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : Vector α n) (x : α) : scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

The recursive step of scanl splits a vector x ::ᵥ v : Vector α (n + 1) into the provided starting value b : β and the recursed scanl f b x : β as the starting value.

This lemma is the cons version of scanl_get.

@[simp]

theorem List.Vector.scanl_val {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) {v : Vector α n} : ↑(scanl f b v) = List.scanl f b ↑v

The underlying List of a Vector after a scanl is the List.scanl of the underlying List of the original Vector.

@[simp]

theorem List.Vector.toList_scanl {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : Vector α n) : (scanl f b v).toList = List.scanl f b v.toList

The toList of a Vector after a scanl is the List.scanl of the toList of the original Vector.

@[simp]

theorem List.Vector.scanl_singleton {α : Type u_1} {β : Type u_6} (f : β → α → β) (b : β) (v : Vector α 1) : scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

The recursive step of scanl splits a vector made up of a single element x ::ᵥ nil : Vector α 1 into a Vector of the provided starting value b : β and the mapped f b x : β as the last value.

@[simp]

theorem List.Vector.scanl_head {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : Vector α n) : (scanl f b v).head = b

The first element of scanl of a vector v : Vector α n, retrieved via head, is the starting value b : β.

@[simp]

theorem List.Vector.scanl_get {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : Vector α n) (i : Fin n) : (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

For an index i : Fin n, the nth element of scanl of a vector v : Vector α n at i.succ, is equal to the application function f : β → α → β of the castSucc i element of scanl f b v and get v i.

This lemma is the get version of scanl_cons.

def List.Vector.mOfFn {m : Type u → Type u_6} [Monad m] {α : Type u} {n : ℕ} : (Fin n → m α) → m (Vector α n)

Monadic analog of Vector.ofFn. Given a monadic function on Fin n, return a Vector α n inside the monad.

Equations

• List.Vector.mOfFn x_2 = pure List.Vector.nil
• List.Vector.mOfFn f = do let a ← f 0 let v ← List.Vector.mOfFn fun (i : Fin n) => f i.succ pure (a ::ᵥ v)

theorem List.Vector.mOfFn_pure {m : Type u_6 → Type u_7} [Monad m] [LawfulMonad m] {α : Type u_6} {n : ℕ} (f : Fin n → α) : (mOfFn fun (i : Fin n) => pure (f i)) = pure (ofFn f)

def List.Vector.mmap {m : Type u → Type u_6} [Monad m] {α : Type u_7} {β : Type u} (f : α → m β) {n : ℕ} : Vector α n → m (Vector β n)

Apply a monadic function to each component of a vector, returning a vector inside the monad.

Equations

• List.Vector.mmap f x_2 = pure List.Vector.nil
• List.Vector.mmap f xs = do let h' ← f xs.head let t' ← List.Vector.mmap f xs.tail pure (h' ::ᵥ t')

@[simp]

theorem List.Vector.mmap_nil {m : Type u_6 → Type u_7} [Monad m] {α : Type u_8} {β : Type u_6} (f : α → m β) : mmap f nil = pure nil

@[simp]

theorem List.Vector.mmap_cons {m : Type u_6 → Type u_7} [Monad m] {α : Type u_8} {β : Type u_6} (f : α → m β) (a : α) {n : ℕ} (v : Vector α n) : mmap f (a ::ᵥ v) = do let h' ← f a let t' ← mmap f v pure (h' ::ᵥ t')

def List.Vector.inductionOn {α : Type u_1} {C : {n : ℕ} → Vector α n → Sort u_6} {n : ℕ} (v : Vector α n) (nil : C nil) (cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)) : C v

Define C v by induction on v : Vector α n.

This function has two arguments: nil handles the base case on C nil, and cons defines the inductive step using ∀ x : α, C w → C (x ::ᵥ w).

It is used as the default induction principle for the induction tactic.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem List.Vector.inductionOn_nil {α : Type u_1} {C : {n : ℕ} → Vector α n → Sort u_6} (nil : C nil) (cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)) : (List.Vector.nil.inductionOn nil fun {n : ℕ} {x : α} {w : Vector α n} => cons) = nil

@[simp]

theorem List.Vector.inductionOn_cons {α : Type u_1} {C : {n : ℕ} → Vector α n → Sort u_6} {n : ℕ} (x : α) (v : Vector α n) (nil : C nil) (cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)) : ((x ::ᵥ v).inductionOn nil fun {n : ℕ} {x : α} {w : Vector α n} => cons) = cons (v.inductionOn nil fun {n : ℕ} {x : α} {w : Vector α n} => cons)

def List.Vector.inductionOn₂ {α : Type u_1} {n : ℕ} {β : Type u_6} {C : {n : ℕ} → Vector α n → Vector β n → Sort u_8} (v : Vector α n) (w : Vector β n) (nil : C nil nil) (cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)) : C v w

Define C v w by induction on a pair of vectors v : Vector α n and w : Vector β n.

Equations

• One or more equations did not get rendered due to their size.

def List.Vector.inductionOn₃ {α : Type u_1} {n : ℕ} {β : Type u_6} {γ : Type u_7} {C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8} (u : Vector α n) (v : Vector β n) (w : Vector γ n) (nil : C nil nil nil) (cons : {n : ℕ} → {a : α} → {b : β} → {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) : C u v w

Define C u v w by induction on a triplet of vectors u : Vector α n, v : Vector β n, and w : Vector γ b.

Equations

• One or more equations did not get rendered due to their size.

def List.Vector.casesOn {α : Type u_1} {m : ℕ} {motive : {n : ℕ} → Vector α n → Sort u_8} (v : Vector α m) (nil : motive nil) (cons : {n : ℕ} → (hd : α) → (tl : Vector α n) → motive (hd ::ᵥ tl)) : motive v

Define motive v by case-analysis on v : Vector α n.

Equations

• List.Vector.casesOn v nil cons = v.inductionOn nil fun (x : ℕ) (hd : α) (tl : List.Vector α x) (x_1 : motive tl) => cons hd tl

def List.Vector.casesOn₂ {α : Type u_1} {m : ℕ} {β : Type u_6} {motive : {n : ℕ} → Vector α n → Vector β n → Sort u_8} (v₁ : Vector α m) (v₂ : Vector β m) (nil : motive nil nil) (cons : {n : ℕ} → (x : α) → (y : β) → (xs : Vector α n) → (ys : Vector β n) → motive (x ::ᵥ xs) (y ::ᵥ ys)) : motive v₁ v₂

Define motive v₁ v₂ by case-analysis on v₁ : Vector α n and v₂ : Vector β n.

Equations

• List.Vector.casesOn₂ v₁ v₂ nil cons = v₁.inductionOn₂ v₂ nil fun (x : ℕ) (x_1 : α) (y : β) (xs : List.Vector α x) (ys : List.Vector β x) (x_2 : motive xs ys) => cons x_1 y xs ys

def List.Vector.casesOn₃ {α : Type u_1} {m : ℕ} {β : Type u_6} {γ : Type u_7} {motive : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8} (v₁ : Vector α m) (v₂ : Vector β m) (v₃ : Vector γ m) (nil : motive nil nil nil) (cons : {n : ℕ} → (x : α) → (y : β) → (z : γ) → (xs : Vector α n) → (ys : Vector β n) → (zs : Vector γ n) → motive (x ::ᵥ xs) (y ::ᵥ ys) (z ::ᵥ zs)) : motive v₁ v₂ v₃

Define motive v₁ v₂ v₃ by case-analysis on v₁ : Vector α n, v₂ : Vector β n, and v₃ : Vector γ n.

Equations

• One or more equations did not get rendered due to their size.

def List.Vector.toArray {α : Type u_1} {n : ℕ} : Vector α n → Array α

Cast a vector to an array.

Equations

• List.Vector.toArray ⟨xs, property⟩ = cast ⋯ xs.toArray

def List.Vector.insertIdx {α : Type u_1} {n : ℕ} (a : α) (i : Fin (n + 1)) (v : Vector α n) : Vector α (n + 1)

v.insertIdx a i inserts a into the vector v at position i (and shifting later components to the right).

Equations

• List.Vector.insertIdx a i v = ⟨(↑v).insertIdx (↑i) a, ⋯⟩

theorem List.Vector.insertIdx_val {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {v : Vector α n} : ↑(insertIdx a i v) = (↑v).insertIdx (↑i) a

@[simp]

theorem List.Vector.eraseIdx_val {α : Type u_1} {n : ℕ} {i : Fin n} {v : Vector α n} : ↑(eraseIdx i v) = (↑v).eraseIdx ↑i

theorem List.Vector.eraseIdx_insertIdx {α : Type u_1} {n : ℕ} {a : α} {v : Vector α n} {i : Fin (n + 1)} : eraseIdx i (insertIdx a i v) = v

theorem List.Vector.eraseIdx_insertIdx' {α : Type u_1} {n : ℕ} {a : α} {v : Vector α (n + 1)} {i : Fin (n + 1)} {j : Fin (n + 2)} : eraseIdx (j.succAbove i) (insertIdx a j v) = insertIdx a (i.predAbove j) (eraseIdx i v)

Erasing an element after inserting an element, at different indices.

theorem List.Vector.insertIdx_comm {α : Type u_1} {n : ℕ} (a b : α) (i j : Fin (n + 1)) (h : i ≤ j) (v : Vector α n) : insertIdx b j.succ (insertIdx a i v) = insertIdx a i.castSucc (insertIdx b j v)

def List.Vector.set {α : Type u_1} {n : ℕ} (v : Vector α n) (i : Fin n) (a : α) : Vector α n

set v n a replaces the nth element of v with a.

Equations

• v.set i a = ⟨(↑v).set (↑i) a, ⋯⟩

@[simp]

theorem List.Vector.toList_set {α : Type u_1} {n : ℕ} (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).toList = v.toList.set (↑i) a

@[simp]

theorem List.Vector.get_set_same {α : Type u_1} {n : ℕ} (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).get i = a

theorem List.Vector.get_set_of_ne {α : Type u_1} {n : ℕ} {v : Vector α n} {i j : Fin n} (h : i ≠ j) (a : α) : (v.set i a).get j = v.get j

theorem List.Vector.get_set_eq_if {α : Type u_1} {n : ℕ} {v : Vector α n} {i j : Fin n} (a : α) : (v.set i a).get j = if i = j then a else v.get j

theorem List.Vector.prod_set {α : Type u_1} {n : ℕ} [Monoid α] (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).toList.prod = (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod

theorem List.Vector.sum_set {α : Type u_1} {n : ℕ} [AddMonoid α] (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).toList.sum = (take (↑i) v).toList.sum + a + (drop (↑i + 1) v).toList.sum

theorem List.Vector.prod_set' {α : Type u_1} {n : ℕ} [CommGroup α] (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a

Variant of List.Vector.prod_set that multiplies by the inverse of the replaced element

theorem List.Vector.sum_set' {α : Type u_1} {n : ℕ} [AddCommGroup α] (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).toList.sum = v.toList.sum + -v.get i + a

Variant of List.Vector.sum_set that subtracts the inverse of the replaced element

def List.Vector.traverse {n : ℕ} {F : Type u → Type u} [Applicative F] {α β : Type u} (f : α → F β) : Vector α n → F (Vector β n)

Apply an applicative function to each component of a vector.

Equations

• List.Vector.traverse f ⟨v, Hv⟩ = cast ⋯ (List.Vector.traverseAux✝ f v)

@[simp]

theorem List.Vector.traverse_def {n : ℕ} {F : Type u → Type u} [Applicative F] {α β : Type u} (f : α → F β) (x : α) (xs : Vector α n) : Vector.traverse f (x ::ᵥ xs) = cons <$> f x <*> Vector.traverse f xs

theorem List.Vector.id_traverse {n : ℕ} {α : Type u} (x : Vector α n) : Vector.traverse pure x = pure x

theorem List.Vector.comp_traverse {n : ℕ} {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : Vector α n) : Vector.traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (Vector.traverse f <$> Vector.traverse g x)

theorem List.Vector.traverse_eq_map_id {n : ℕ} {α β : Type u_6} (f : α → β) (x : Vector α n) : Vector.traverse (pure ∘ f) x = pure (map f x)

theorem List.Vector.naturality {n : ℕ} {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative G] [LawfulApplicative F] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : Vector α n) : (fun {α : Type u} => η.app α) (Vector.traverse f x) = Vector.traverse ((fun {α : Type u} => η.app α) ∘ f) x

instance List.Vector.instTraversableFlipNat {n : ℕ} : Traversable (flip Vector n)

Equations

• List.Vector.instTraversableFlipNat = { map := fun {α β : Type ?u.15} => List.Vector.map, traverse := @List.Vector.traverse n }

instance List.Vector.instLawfulTraversableFlipNat {n : ℕ} : LawfulTraversable (flip Vector n)

@[simp]

theorem List.Vector.replicate_succ {α : Type u_1} {n : ℕ} (val : α) : replicate (n + 1) val = val ::ᵥ replicate n val

@[simp]

theorem List.Vector.get_append_cons_zero {α : Type u_1} {m n : ℕ} {x : α} (xs : Vector α n) (ys : Vector α m) : ((x ::ᵥ xs).append ys).get 0 = x

@[simp]

theorem List.Vector.get_append_cons_succ {α : Type u_1} {m n : ℕ} {x : α} (xs : Vector α n) (ys : Vector α m) {i : Fin (n + m)} {h : ↑i + 1 < n.succ + m} : ((x ::ᵥ xs).append ys).get ⟨↑i + 1, h⟩ = (xs.append ys).get i

@[simp]

theorem List.Vector.append_nil {α : Type u_1} {n : ℕ} (xs : Vector α n) : xs.append nil = xs

@[simp]

theorem List.Vector.get_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (v₁ : Vector α n) (v₂ : Vector β n) (f : α → β → γ) (i : Fin n) : (map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)

@[simp]

theorem List.Vector.mapAccumr_cons {α : Type u_1} {β : Type u_2} {σ : Type u_4} {n : ℕ} {x : α} {s : σ} (xs : Vector α n) {f : α → σ → σ × β} : mapAccumr f (x ::ᵥ xs) s = let r := mapAccumr f xs s; let q := f x r.1; (q.1, q.2 ::ᵥ r.2)

@[simp]

theorem List.Vector.mapAccumr₂_cons {α : Type u_1} {β : Type u_2} {σ : Type u_4} {φ : Type u_5} {n : ℕ} {x : α} {y : β} {s : σ} (xs : Vector α n) (ys : Vector β n) {f : α → β → σ → σ × φ} : mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s = let r := mapAccumr₂ f xs ys s; let q := f x y r.1; (q.1, q.2 ::ᵥ r.2)