English
Variant of prod_set for a commutative group: the product equals the original product times the inverse of the replaced element times a.
Русский
Вариант prod_set' для коммутативной группы: произведение равно исходному произведению умноженному на обратное замещаемого элемента и на a.
LaTeX
$$$ (v.set i a).toList.prod = v.toList.prod \\cdot (v.get i)^{-1} \\cdot a $$$
Lean4
/-- Variant of `List.Vector.prod_set` that multiplies by the inverse of the replaced element -/
@[to_additive /-- Variant of `List.Vector.sum_set` that subtracts the inverse of the replaced element -/
]
theorem prod_set' [CommGroup α] (v : Vector α n) (i : Fin n) (a : α) :
(v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a :=
by
refine (List.prod_set' v.toList i a).trans ?_
simp [get_eq_get_toList, mul_assoc]
