English
Let L be a list in a monoid M, n an index, and a ∈ M. After replacing the nth element by a, the new product is given by the prefix, the replacement (if in range), and the tail: (L.set n a).prod = ((L.take n).prod * (if n < length L then a else 1)) * (L.drop (n+1)).prod.
Русский
Пусть L — список в моноиде M, n — индекс и a — элемент. После замены n-го элемента на a новое произведение равно произведению префикса, заменённого элемента (если он существует) и хвоста: (L.set n a).prod = ((L.take n).prod · (если n < длина L тогда a иначе 1)) · (L.drop (n+1)).prod.
LaTeX
$$$ (L.set n a).prod = \bigl((L.take n).prod \cdot \text{if } n < L.length \text{ then } a \text{ else } 1\bigr) \cdot (L.drop (n + 1)).prod $$$
Lean4
@[to_additive]
theorem prod_set :
∀ (L : List M) (n : ℕ) (a : M),
(L.set n a).prod = ((L.take n).prod * if n < L.length then a else 1) * (L.drop (n + 1)).prod
| x :: xs, 0, a => by simp [set]
| x :: xs, i + 1, a => by simp [set, prod_set xs i a, mul_assoc, Nat.add_lt_add_iff_right]
| [], _, _ => by simp [set, (Nat.zero_le _).not_gt]
