English
The product of a finite set of terms each equal to either f(i) or 0 is zero unless all conditions p(i) hold; when p(i) holds for all i in s, the product equals the product of f(i).
Русский
Произведение над Finset из выражений if p(i) then f(i) else 0 равно 0, если не выполняется p(i) для некоторого i; иначе равно произведению f(i).
LaTeX
$$$\\prod_{i\\in s} \\Big(\\operatorname{ite}(p(i), f(i), 0)\\Big) = \\operatorname{ite}\\Big(\\forall i\\in s, p(i)\\Big, \\prod_{i\\in s} f(i), 0\\Big)$$$
Lean4
theorem prod_ite_zero : (∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0 :=
by
split_ifs with h
· exact prod_congr rfl fun i hi => by simp [h i hi]
· push_neg at h
rcases h with ⟨i, hi, hq⟩
exact prod_eq_zero hi (by simp [hq])
