prod_eq_mul_prod_diff_singleton — Mathlib

English

If i is an element of a finite set s and f: ι → M, then the product over s equals f(i) times the product over s without i: ∏ x∈s f(x) = f(i) · ∏ x∈s\\{i} f(x).

Русский

Пусть i ∈ s и f : ι → M; тогда произведение по x∈s f(x) равно f(i) умножить на произведение по x∈s\\{i} f(x).

LaTeX

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

Lean4

@[to_additive]
theorem prod_eq_mul_prod_diff_singleton [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) :
    ∏ x ∈ s, f x = f i * ∏ x ∈ s \ { i }, f x :=
  by
  convert (s.prod_inter_mul_prod_diff { i } f).symm
  simp [h]

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