prod_update_of_mem — Mathlib

English

If i ∈ s, then ∏ x∈s update f i b x = b * ∏ x∈s\\{i} f x.

Русский

Если i ∈ s, то произведение по s после обновления f в i равно b умножить на произведение по s\\{i} f(x).

LaTeX

$$$\\displaystyle \\prod_{x \\in s} \\mathrm{update}\\, f\\, i\\, b\\, x = b \\cdot \\prod_{x \\in s \\setminus \\{i\\}} f(x)$$$

Lean4

@[to_additive]
theorem prod_update_of_mem [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) (b : M) :
    ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ singleton i, f x :=
  by
  rw [update_eq_piecewise, prod_piecewise]
  simp [h]

Похожие утверждения