English
A simplification variant: the dite equality with equality tests on indices reduces to a simple product with an indicator for membership.
Русский
Упрощение: равенство dite с тестами равенства индексов сводится к простому произведению с индикацией принадлежности.
LaTeX
$$$\\prod_{x \\in s} \\bigl(\\text{if } h : x = a \\text{ then } b(x,h) \\text{ else } 1\\bigr) = \\text{ite}(a \\in s) (b(a, rfl)) 1.$$$
Lean4
/-- A product taken over a conditional whose condition is an equality test on the index and whose
alternative is `1` has value either the term at that index or `1`.
The difference with `Finset.prod_ite_eq` is that the arguments to `Eq` are swapped. -/
@[to_additive (attr := simp) /-- A sum taken over a conditional whose condition is an equality
test on the index and whose alternative is `0` has value either the term at that index or `0`.
The difference with `Finset.sum_ite_eq` is that the arguments to `Eq` are swapped. -/
]
theorem prod_ite_eq' [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) :
(∏ x ∈ s, ite (x = a) (b x) 1) = ite (a ∈ s) (b a) 1 :=
prod_dite_eq' s a fun x _ => b x
