English
For f : α → M and a ∈ α with DecidableEq α and hf : (mulSupport f).Finite, the finprod over all i ≠ a equals the product over the finite set hf.toFinset.erase a.
Русский
Для f : α → M и элемента a с конечным множеством поддержки, финпроизводство по i ≠ a равно произведению по hf.toFinset.erase a.
LaTeX
$$$$ \prod^{\mathrm{fin}}_{i} (i \neq a) f(i) = \prod_{i \in hf.toFinset.erase a} f(i). $$$$
Lean4
@[to_additive]
theorem finprod_cond_ne (f : α → M) (a : α) [DecidableEq α] (hf : (mulSupport f).Finite) :
(∏ᶠ (i) (_ : i ≠ a), f i) = ∏ i ∈ hf.toFinset.erase a, f i :=
by
apply finprod_cond_eq_prod_of_cond_iff
intro x hx
rw [Finset.mem_erase, Finite.mem_toFinset, mem_mulSupport]
grind
