English
A restatement of the product with the equality test reversed: (f.prod (λ x v, ite (x = a) (b x v) 1)) equals b a (f a) if a is in the support, otherwise 1.
Русский
Переформулировка произведения с обратной проверкой равенства: (f.prod (λ x v, ite (x = a) (b x v) 1)) равно b(a, f(a)) если a ∈ поддержка, иначе 1.
LaTeX
$$$$ (f \\mathrm{prod} (\\\\lambda x v. \\\\text{ite}(x = a) (b x v) 1)) = \\\\begin{cases} b(a, f(a)) & a \\in \\mathrm{supp}(f), \\\\ 1 & \\text{иначе}. \\end{cases} $$$$
Lean4
/-- A restatement of `prod_ite_eq` with the equality test reversed. -/
@[to_additive (attr := simp) /-- A restatement of `sum_ite_eq` with the equality test reversed. -/
]
theorem prod_ite_eq' [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) :
(f.prod fun x v => ite (x = a) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 :=
by
dsimp [Finsupp.prod]
rw [f.support.prod_ite_eq']
