English
In a vector, replacing the i-th element by a multiplies the product of all elements accordingly: prod equals take i, then multiply by a, then drop tail.
Русский
При замене i-й позиции на a произведение элементов вектора меняется соответствующим образом: произведение равно произведению первых i элементов умноженным на a и на оставшиеся.
LaTeX
$$$ (v.set i a).toList.prod = (v.take i).toList.prod \\cdot a \\cdot (v.drop (i+1)).toList.prod $$$
Lean4
@[to_additive]
theorem prod_set [Monoid α] (v : Vector α n) (i : Fin n) (a : α) :
(v.set i a).toList.prod = (v.take i).toList.prod * a * (v.drop (i + 1)).toList.prod :=
by
refine (List.prod_set v.toList i a).trans ?_
simp_all
