English
If we replace the nth element of a list by a, the product of the new list equals the old product multiplied by a certain factor depending on whether n is within bounds.
Русский
Если заменить n-й элемент списка на a, произведение новой последовательности равно старому произведению, умноженному на некоторый множитель в зависимости от того, находится ли n в пределах длины списка.
LaTeX
$$(L.set n a).prod = L.prod * if hn : n < L.length then L[n]^{-1} * a else 1$$
Lean4
/-- Alternative version of `List.prod_set` when the list is over a group -/
@[to_additive /-- Alternative version of `List.sum_set` when the list is over a group -/
]
theorem prod_set' (L : List G) (n : ℕ) (a : G) :
(L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1 :=
by
refine (prod_set L n a).trans ?_
split_ifs with hn
·
rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ← mul_assoc (take n L).prod,
prod_take_mul_prod_drop, mul_comm a, mul_assoc]
·
simp only [take_of_length_le (le_of_not_gt hn), prod_nil, mul_one,
drop_eq_nil_of_le ((le_of_not_gt hn).trans n.le_succ)]
