English
Replacing the nth element of a list with a yields the new product equal to the old product multiplied by the inverse of the old nth element times a, when n is within bounds; otherwise the product remains unchanged.
Русский
Замена n-го элемента списка на a приводит к произведению, равному старому произведению, умноженному на обратное старого n-го элемента, умноженное на a, если n в пределах длины списка; иначе произведение не меняется.
LaTeX
$$(L.set n a).prod = L.prod \cdot (if hn : n < L.length then L[n]^{-1} * a else 1)$$
Lean4
/-- This is the `List.prod` version of `mul_inv` -/
@[to_additive /-- This is the `List.sum` version of `add_neg` -/
]
theorem prod_inv {K : Type*} [DivisionCommMonoid K] : ∀ L : List K, L.prod⁻¹ = (L.map fun x => x⁻¹).prod
| [] => by simp
| x :: xs => by simp [mul_comm, prod_inv xs]
