toList_set — Mathlib

English

Applying set to a vector and then converting to a list yields the same result as setting in the list and converting back.

Русский

После применения set к вектору и последующего преобразования в список получаем тот же результат, что и при изменении списка и последующем конвертировании обратно.

LaTeX

$$$ (v.set i a).\\toList = v.\\toList.set i a $$$

Lean4

@[simp]
theorem toList_set (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).toList = v.toList.set i a :=
  rfl

Похожие утверждения