# Additional theorems and definitions about the Vector type #

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

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
Instances For
instance Mathlib.Vector.instInhabited {α : Type u_1} {n : } [] :
Equations
theorem Mathlib.Vector.toList_injective {α : Type u_1} {n : } :
Function.Injective Mathlib.Vector.toList
theorem Mathlib.Vector.ext_iff {α : Type u_1} {n : } {v : } {w : } :
v = w ∀ (m : Fin n), v.get m = w.get m
theorem Mathlib.Vector.ext {α : Type u_1} {n : } {v : } {w : } :
(∀ (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.

The empty Vector is a Subsingleton.

Equations
• =
@[simp]
theorem Mathlib.Vector.cons_val {α : Type u_1} {n : } (a : α) (v : ) :
(a ::ᵥ v) = a :: v
theorem Mathlib.Vector.eq_cons_iff {α : Type u_1} {n : } (a : α) (v : Mathlib.Vector α n.succ) (v' : ) :
v = a ::ᵥ v' v.head = a v.tail = v'
theorem Mathlib.Vector.ne_cons_iff {α : Type u_1} {n : } (a : α) (v : Mathlib.Vector α n.succ) (v' : ) :
v a ::ᵥ v' v.head a v.tail v'
theorem Mathlib.Vector.exists_eq_cons {α : Type u_1} {n : } (v : Mathlib.Vector α n.succ) :
∃ (a : α) (as : ), v = a ::ᵥ as
@[simp]
theorem Mathlib.Vector.toList_ofFn {α : Type u_1} {n : } (f : Fin nα) :
.toList =
@[simp]
theorem Mathlib.Vector.mk_toList {α : Type u_1} {n : } (v : ) (h : v.toList.length = n) :
v.toList, h = v
@[simp]
theorem Mathlib.Vector.length_val {α : Type u_1} {n : } (v : ) :
(↑v).length = n
@[simp]
theorem Mathlib.Vector.toList_map {α : Type u_1} {n : } {β : Type u_6} (v : ) (f : αβ) :
.toList = List.map f v.toList
@[simp]
theorem Mathlib.Vector.head_map {α : Type u_1} {n : } {β : Type u_6} (v : Mathlib.Vector α (n + 1)) (f : αβ) :
@[simp]
theorem Mathlib.Vector.tail_map {α : Type u_1} {n : } {β : Type u_6} (v : Mathlib.Vector α (n + 1)) (f : αβ) :
.tail = Mathlib.Vector.map f v.tail
theorem Mathlib.Vector.get_eq_get {α : Type u_1} {n : } (v : ) (i : Fin n) :
v.get i = v.toList.get (Fin.cast i)
@[simp]
theorem Mathlib.Vector.get_replicate {α : Type u_1} {n : } (a : α) (i : Fin n) :
.get i = a
@[simp]
theorem Mathlib.Vector.get_map {α : Type u_1} {n : } {β : Type u_6} (v : ) (f : αβ) (i : Fin n) :
.get i = f (v.get i)
@[simp]
theorem Mathlib.Vector.map₂_nil {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) :
Mathlib.Vector.map₂ f Mathlib.Vector.nil Mathlib.Vector.nil = Mathlib.Vector.nil
@[simp]
theorem Mathlib.Vector.map₂_cons {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (hd₁ : α) (tl₁ : ) (hd₂ : β) (tl₂ : ) (f : αβγ) :
Mathlib.Vector.map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ Mathlib.Vector.map₂ f tl₁ tl₂
@[simp]
theorem Mathlib.Vector.get_ofFn {α : Type u_1} {n : } (f : Fin nα) (i : Fin n) :
.get i = f i
@[simp]
theorem Mathlib.Vector.ofFn_get {α : Type u_1} {n : } (v : ) :
def Equiv.vectorEquivFin (α : Type u_6) (n : ) :
(Fin nα)

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

Equations
• = { toFun := Mathlib.Vector.get, invFun := Mathlib.Vector.ofFn, left_inv := , right_inv := }
Instances For
theorem Mathlib.Vector.get_tail {α : Type u_1} {n : } (x : ) (i : Fin (n - 1)) :
x.tail.get i = x.get i + 1,
@[simp]
theorem Mathlib.Vector.get_tail_succ {α : Type u_1} {n : } (v : Mathlib.Vector α n.succ) (i : Fin n) :
v.tail.get i = v.get i.succ
@[simp]
theorem Mathlib.Vector.tail_val {α : Type u_1} {n : } (v : Mathlib.Vector α n.succ) :
v.tail = (↑v).tail
@[simp]
theorem Mathlib.Vector.tail_nil {α : Type u_1} :
Mathlib.Vector.nil.tail = Mathlib.Vector.nil

The tail of a nil vector is nil.

@[simp]
theorem Mathlib.Vector.singleton_tail {α : Type u_1} (v : ) :
v.tail = Mathlib.Vector.nil

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

@[simp]
theorem Mathlib.Vector.tail_ofFn {α : Type u_1} {n : } (f : Fin n.succα) :
.tail = Mathlib.Vector.ofFn fun (i : Fin n) => f i.succ
@[simp]
theorem Mathlib.Vector.toList_empty {α : Type u_1} (v : ) :
v.toList = []
@[simp]
theorem Mathlib.Vector.toList_singleton {α : Type u_1} (v : ) :

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 Mathlib.Vector.empty_toList_eq_ff {α : Type u_1} {n : } (v : Mathlib.Vector α (n + 1)) :
v.toList.isEmpty = false
theorem Mathlib.Vector.not_empty_toList {α : Type u_1} {n : } (v : Mathlib.Vector α (n + 1)) :
¬v.toList.isEmpty = true
@[simp]
theorem Mathlib.Vector.map_id {α : Type u_1} {n : } (v : ) :
= v

Mapping under id does not change a vector.

theorem Mathlib.Vector.nodup_iff_injective_get {α : Type u_1} {n : } {v : } :
v.toList.Nodup Function.Injective v.get
theorem Mathlib.Vector.head?_toList {α : Type u_1} {n : } (v : Mathlib.Vector α n.succ) :
def Mathlib.Vector.reverse {α : Type u_1} {n : } (v : ) :

Reverse a vector.

Equations
• v.reverse = v.toList.reverse,
Instances For
theorem Mathlib.Vector.toList_reverse {α : Type u_1} {n : } {v : } :
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 Mathlib.Vector.reverse_reverse {α : Type u_1} {n : } {v : } :
v.reverse.reverse = v
@[simp]
theorem Mathlib.Vector.get_zero {α : Type u_1} {n : } (v : Mathlib.Vector α n.succ) :
@[simp]
theorem Mathlib.Vector.head_ofFn {α : Type u_1} {n : } (f : Fin n.succα) :
theorem Mathlib.Vector.get_cons_zero {α : Type u_1} {n : } (a : α) (v : ) :
(a ::ᵥ v).get 0 = a
@[simp]
theorem Mathlib.Vector.get_cons_nil {α : Type u_1} {ix : Fin 1} (x : α) :
(x ::ᵥ Mathlib.Vector.nil).get ix = x

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

@[simp]
theorem Mathlib.Vector.get_cons_succ {α : Type u_1} {n : } (a : α) (v : ) (i : Fin n) :
(a ::ᵥ v).get i.succ = v.get i
def Mathlib.Vector.last {α : Type u_1} {n : } (v : Mathlib.Vector α (n + 1)) :
α

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

Equations
Instances For
theorem Mathlib.Vector.last_def {α : Type u_1} {n : } {v : Mathlib.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 Mathlib.Vector.reverse_get_zero {α : Type u_1} {n : } {v : Mathlib.Vector α (n + 1)} :

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

def Mathlib.Vector.scanl {α : Type u_1} {n : } {β : Type u_6} (f : βαβ) (b : β) (v : ) :
Mathlib.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
Instances For
@[simp]
theorem Mathlib.Vector.scanl_nil {α : Type u_1} {β : Type u_6} (f : βαβ) (b : β) :
Mathlib.Vector.scanl f b Mathlib.Vector.nil = b ::ᵥ Mathlib.Vector.nil

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

@[simp]
theorem Mathlib.Vector.scanl_cons {α : Type u_1} {n : } {β : Type u_6} (f : βαβ) (b : β) (v : ) (x : α) :

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 Mathlib.Vector.scanl_val {α : Type u_1} {n : } {β : Type u_6} (f : βαβ) (b : β) {v : } :
(Mathlib.Vector.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 Mathlib.Vector.toList_scanl {α : Type u_1} {n : } {β : Type u_6} (f : βαβ) (b : β) (v : ) :
(Mathlib.Vector.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 Mathlib.Vector.scanl_singleton {α : Type u_1} {β : Type u_6} (f : βαβ) (b : β) (v : ) :
= b ::ᵥ f b v.head ::ᵥ Mathlib.Vector.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 Mathlib.Vector.scanl_head {α : Type u_1} {n : } {β : Type u_6} (f : βαβ) (b : β) (v : ) :
(Mathlib.Vector.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 Mathlib.Vector.scanl_get {α : Type u_1} {n : } {β : Type u_6} (f : βαβ) (b : β) (v : ) (i : Fin n) :
(Mathlib.Vector.scanl f b v).get i.succ = f ((Mathlib.Vector.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 Mathlib.Vector.mOfFn {m : Type u → Type u_6} [] {α : Type u} {n : } :
(Fin nm α)m (Mathlib.Vector α n)

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

Equations
Instances For
theorem Mathlib.Vector.mOfFn_pure {m : Type u_6 → Type u_7} [] [] {α : Type u_6} {n : } (f : Fin nα) :
(Mathlib.Vector.mOfFn fun (i : Fin n) => pure (f i)) =
def Mathlib.Vector.mmap {m : Type u → Type u_6} [] {α : Type u_7} {β : Type u} (f : αm β) {n : } :
m (Mathlib.Vector β n)

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

Equations
Instances For
@[simp]
theorem Mathlib.Vector.mmap_nil {m : Type u_6 → Type u_7} [] {α : Type u_8} {β : Type u_6} (f : αm β) :
Mathlib.Vector.mmap f Mathlib.Vector.nil = pure Mathlib.Vector.nil
@[simp]
theorem Mathlib.Vector.mmap_cons {m : Type u_6 → Type u_7} [] {α : Type u_8} {β : Type u_6} (f : αm β) (a : α) {n : } (v : ) :
Mathlib.Vector.mmap f (a ::ᵥ v) = do let h'f a let t' pure (h' ::ᵥ t')
def Mathlib.Vector.inductionOn {α : Type u_1} {C : {n : } → Sort u_6} {n : } (v : ) (nil : C Mathlib.Vector.nil) (cons : {n : } → {x : α} → {w : } → C wC (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.
Instances For
@[simp]
theorem Mathlib.Vector.inductionOn_nil {α : Type u_1} {C : {n : } → Sort u_6} (nil : C Mathlib.Vector.nil) (cons : {n : } → {x : α} → {w : } → C wC (x ::ᵥ w)) :
(Mathlib.Vector.nil.inductionOn nil fun {n : } {x : α} {w : } => cons) = nil
@[simp]
theorem Mathlib.Vector.inductionOn_cons {α : Type u_1} {C : {n : } → Sort u_6} {n : } (x : α) (v : ) (nil : C Mathlib.Vector.nil) (cons : {n : } → {x : α} → {w : } → C wC (x ::ᵥ w)) :
((x ::ᵥ v).inductionOn nil fun {n : } {x : α} {w : } => cons) = cons (v.inductionOn nil fun {n : } {x : α} {w : } => cons)
def Mathlib.Vector.inductionOn₂ {α : Type u_1} {n : } {β : Type u_6} {C : {n : } → Sort u_8} (v : ) (w : ) (nil : C Mathlib.Vector.nil Mathlib.Vector.nil) (cons : {n : } → {a : α} → {b : β} → {x : } → {y : } → C x yC (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.
Instances For
def Mathlib.Vector.inductionOn₃ {α : Type u_1} {n : } {β : Type u_6} {γ : Type u_7} {C : {n : } → Sort u_8} (u : ) (v : ) (w : ) (nil : C Mathlib.Vector.nil Mathlib.Vector.nil Mathlib.Vector.nil) (cons : {n : } → {a : α} → {b : β} → {c : γ} → {x : } → {y : } → {z : } → C x y zC (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.
Instances For
def Mathlib.Vector.casesOn {α : Type u_1} {m : } {motive : {n : } → Sort u_8} (v : ) (nil : motive Mathlib.Vector.nil) (cons : {n : } → (hd : α) → (tl : ) → motive (hd ::ᵥ tl)) :
motive v

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

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

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

Equations
• Mathlib.Vector.casesOn₂ v₁ v₂ nil cons = v₁.inductionOn₂ v₂ nil fun (x : ) (x_1 : α) (y : β) (xs : ) (ys : ) (x_2 : motive xs ys) => cons x_1 y xs ys
Instances For
def Mathlib.Vector.casesOn₃ {α : Type u_1} {m : } {β : Type u_6} {γ : Type u_7} {motive : {n : } → Sort u_8} (v₁ : ) (v₂ : ) (v₃ : ) (nil : motive Mathlib.Vector.nil Mathlib.Vector.nil Mathlib.Vector.nil) (cons : {n : } → (x : α) → (y : β) → (z : γ) → (xs : ) → (ys : ) → (zs : ) → 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.
Instances For
def Mathlib.Vector.toArray {α : Type u_1} {n : } :

Cast a vector to an array.

Equations
Instances For
def Mathlib.Vector.insertNth {α : Type u_1} {n : } (a : α) (i : Fin (n + 1)) (v : ) :
Mathlib.Vector α (n + 1)

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

Equations
Instances For
theorem Mathlib.Vector.insertNth_val {α : Type u_1} {n : } {a : α} {i : Fin (n + 1)} {v : } :
= List.insertNth (↑i) a v
@[simp]
theorem Mathlib.Vector.eraseIdx_val {α : Type u_1} {n : } {i : Fin n} {v : } :
= (↑v).eraseIdx i
@[deprecated Mathlib.Vector.eraseIdx_val]
theorem Mathlib.Vector.removeNth_val {α : Type u_1} {n : } {i : Fin n} {v : } :
= (↑v).eraseIdx i

Alias of Mathlib.Vector.eraseIdx_val.

theorem Mathlib.Vector.eraseIdx_insertNth {α : Type u_1} {n : } {a : α} {v : } {i : Fin (n + 1)} :
= v
@[deprecated Mathlib.Vector.eraseIdx_insertNth]
theorem Mathlib.Vector.removeNth_insertNth {α : Type u_1} {n : } {a : α} {v : } {i : Fin (n + 1)} :
= v

Alias of Mathlib.Vector.eraseIdx_insertNth.

theorem Mathlib.Vector.eraseIdx_insertNth' {α : Type u_1} {n : } {a : α} {v : Mathlib.Vector α (n + 1)} {i : Fin (n + 1)} {j : Fin (n + 2)} :
Mathlib.Vector.eraseIdx (j.succAbove i) = Mathlib.Vector.insertNth a (i.predAbove j)
@[deprecated Mathlib.Vector.eraseIdx_insertNth']
theorem Mathlib.Vector.removeNth_insertNth' {α : Type u_1} {n : } {a : α} {v : Mathlib.Vector α (n + 1)} {i : Fin (n + 1)} {j : Fin (n + 2)} :
Mathlib.Vector.eraseIdx (j.succAbove i) = Mathlib.Vector.insertNth a (i.predAbove j)

Alias of Mathlib.Vector.eraseIdx_insertNth'.

theorem Mathlib.Vector.insertNth_comm {α : Type u_1} {n : } (a : α) (b : α) (i : Fin (n + 1)) (j : Fin (n + 1)) (h : i j) (v : ) :
def Mathlib.Vector.set {α : Type u_1} {n : } (v : ) (i : Fin n) (a : α) :

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

Equations
• v.set i a = (↑v).set (↑i) a,
Instances For
@[simp]
theorem Mathlib.Vector.toList_set {α : Type u_1} {n : } (v : ) (i : Fin n) (a : α) :
(v.set i a).toList = v.toList.set (↑i) a
@[simp]
theorem Mathlib.Vector.get_set_same {α : Type u_1} {n : } (v : ) (i : Fin n) (a : α) :
(v.set i a).get i = a
theorem Mathlib.Vector.get_set_of_ne {α : Type u_1} {n : } {v : } {i : Fin n} {j : Fin n} (h : i j) (a : α) :
(v.set i a).get j = v.get j
theorem Mathlib.Vector.get_set_eq_if {α : Type u_1} {n : } {v : } {i : Fin n} {j : Fin n} (a : α) :
(v.set i a).get j = if i = j then a else v.get j
theorem Mathlib.Vector.sum_set {α : Type u_1} {n : } [] (v : ) (i : Fin n) (a : α) :
(v.set i a).toList.sum = (Mathlib.Vector.take (↑i) v).toList.sum + a + (Mathlib.Vector.drop (i + 1) v).toList.sum
theorem Mathlib.Vector.prod_set {α : Type u_1} {n : } [] (v : ) (i : Fin n) (a : α) :
(v.set i a).toList.prod = (Mathlib.Vector.take (↑i) v).toList.prod * a * (Mathlib.Vector.drop (i + 1) v).toList.prod
theorem Mathlib.Vector.sum_set' {α : Type u_1} {n : } [] (v : ) (i : Fin n) (a : α) :
(v.set i a).toList.sum = v.toList.sum + -v.get i + a
theorem Mathlib.Vector.prod_set' {α : Type u_1} {n : } [] (v : ) (i : Fin n) (a : α) :
(v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a
def Mathlib.Vector.traverse {n : } {F : Type u → Type u} [] {α : Type u} {β : Type u} (f : αF β) :
F (Mathlib.Vector β n)

Apply an applicative function to each component of a vector.

Equations
Instances For
@[simp]
theorem Mathlib.Vector.traverse_def {n : } {F : Type u → Type u} [] {α : Type u} {β : Type u} (f : αF β) (x : α) (xs : ) :
Mathlib.Vector.traverse f (x ::ᵥ xs) = Seq.seq (Mathlib.Vector.cons <\$> f x) fun (x : Unit) =>
theorem Mathlib.Vector.id_traverse {n : } {α : Type u} (x : ) :
= x
theorem Mathlib.Vector.comp_traverse {n : } {F : Type u → Type u} {G : Type u → Type u} [] [] {α : Type u} {β : Type u} {γ : Type u} (f : βF γ) (g : αG β) (x : ) :
Mathlib.Vector.traverse (Functor.Comp.mk g) x =
theorem Mathlib.Vector.traverse_eq_map_id {n : } {α : Type u_6} {β : Type u_6} (f : αβ) (x : ) :
theorem Mathlib.Vector.naturality {n : } {F : Type u → Type u} {G : Type u → Type u} [] [] (η : ) {α : Type u} {β : Type u} (f : αF β) (x : ) :
(fun {α : Type u} => η.app α) = Mathlib.Vector.traverse ((fun {α : Type u} => η.app α) f) x
Equations
• Mathlib.Vector.instTraversableFlipNat =
@[simp]
theorem Mathlib.Vector.replicate_succ {α : Type u_1} {n : } (val : α) :
@[simp]
theorem Mathlib.Vector.get_append_cons_zero {α : Type u_1} {m : } {n : } {x : α} (xs : ) (ys : ) :
((x ::ᵥ xs).append ys).get 0, = x
@[simp]
theorem Mathlib.Vector.get_append_cons_succ {α : Type u_1} {m : } {n : } {x : α} (xs : ) (ys : ) {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 Mathlib.Vector.append_nil {α : Type u_1} {n : } (xs : ) :
xs.append Mathlib.Vector.nil = xs
@[simp]
theorem Mathlib.Vector.get_map₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (v₁ : ) (v₂ : ) (f : αβγ) (i : Fin n) :
(Mathlib.Vector.map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)
@[simp]
theorem Mathlib.Vector.mapAccumr_cons {α : Type u_1} {β : Type u_2} {σ : Type u_4} {n : } {x : α} {s : σ} (xs : ) {f : ασσ × β} :
Mathlib.Vector.mapAccumr f (x ::ᵥ xs) s = let r := ; let q := f x r.1; (q.1, q.2 ::ᵥ r.2)
@[simp]
theorem Mathlib.Vector.mapAccumr₂_cons {α : Type u_1} {β : Type u_2} {σ : Type u_4} {φ : Type u_5} {n : } {x : α} {y : β} {s : σ} (xs : ) (ys : ) {f : αβσσ × φ} :
Mathlib.Vector.mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s = let r := ; let q := f x y r.1; (q.1, q.2 ::ᵥ r.2)