@[inline]

def Vector.modify {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (f : α → α) : Vector α n

In-place update of the element at index i via f, wrapping Array.modify so the underlying swap-with-placeholder ownership transfer survives codegen. Calling xs.set i (f xs[i]) forces a lean_inc on the borrowed entry and loses uniqueness on nested-array shapes (e.g. matrix rows); modify avoids that copy when xs is uniquely owned.

Equations

• xs.modify i f = Vector.mk (xs.toArray.modify i f) ⋯

theorem Vector.getElem_modify {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {f : α → α} {j : Nat} (hj : j < n) : (xs.modify i f)[j] = if i = j then f xs[j] else xs[j]

Entrywise read of modify: the modified index gets f applied, every other index is unchanged.

theorem Vector.getElem_modify_self {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {f : α → α} (hi : i < n) : (xs.modify i f)[i] = f xs[i]

The modified index of modify reads back f applied to the old value.

theorem Vector.getElem_modify_of_ne {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} {f : α → α} (hj : j < n) (h : i ≠ j) : (xs.modify i f)[j] = xs[j]

Any index other than the modified one is unchanged by modify.

theorem Vector.modify_eq_set {α : Type u_1} {n : Nat} (xs : Vector α n) (i : Nat) (f : α → α) (h : i < n) : xs.modify i f = xs.set i (f xs[i]) h

modify agrees with the read-then-set form (value-level; modify avoids the copy this form would force).

theorem Vector.getElem_foldl_modify_not_mem {n : Nat} {α : Type u_1} (g : Fin n → α → α) {r : Nat} (hr : r < n) (xs : List (Fin n)) (v0 : Vector α n) : (∀ (i : Fin n), i ∈ xs → ↑i ≠ r) → (List.foldl (fun (v : Vector α n) (i : Fin n) => v.modify (↑i) (g i)) v0 xs)[r] = v0[r]

A left fold of per-index modifys over a list of Fin n indices leaves index r untouched when r is not among the folded indices. The backing engine for the in-place indexed row scatter (Matrix.mapRowsIdx).

theorem Vector.getElem_foldl_modify_mem {n : Nat} {α : Type u_1} (g : Fin n → α → α) (xs : List (Fin n)) : xs.Nodup → ∀ (v0 : Vector α n) (r : Fin n), r ∈ xs → (List.foldl (fun (v : Vector α n) (i : Fin n) => v.modify (↑i) (g i)) v0 xs)[↑r] = g r v0[↑r]

A left fold of per-index modifys over a Nodup list writes g r at every member index r (reading the value r held before the fold, since each index is visited at most once).

theorem Vector.getElem_finFoldl_modify {α : Type u_1} {n : Nat} (v0 : Vector α n) (g : Fin n → α → α) (r : Fin n) : (Fin.foldl n (fun (v : Vector α n) (i : Fin n) => v.modify (↑i) (g i)) v0)[↑r] = g r v0[↑r]

Reading index r of a Fin.foldl of per-index modifys yields g r applied to the original entry — every index is visited exactly once. This is the in-place (no intermediate List.finRange allocation) scatter form.