prod_eq_prod_diff_singleton_mul — Mathlib

English

Let s be a finite set of indices with i ∈ s. Then ∏ x∈s f(x) equals (∏ x∈s\\{i} f(x)) · f(i).

Русский

Пусть s — конечное множество индексов и i ∈ s. Тогда ∏_{x∈s} f(x) = (∏_{x∈s\\{i}} f(x)) · f(i).

LaTeX

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

Lean4

@[to_additive]
theorem prod_eq_prod_diff_singleton_mul [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∈ s) (f : ι → M) :
    ∏ x ∈ s, f x = (∏ x ∈ s \ { i }, f x) * f i := by rw [prod_eq_mul_prod_diff_singleton h, mul_comm]

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