English
If y ∈ support(f), then g(y, f(y)) · (erase y f).prod g = f.prod g. Intuitively, removing a nonzero coordinate and multiplying by its value restores the full product.
Русский
Пусть y принадлежит поддержке f. Тогда g(y, f(y))·(erase y f).prod g = f.prod g. Интуитивно — удаление ненулевой координаты и умножение её значения возвращают полное произведение.
LaTeX
$$$$ g(y, f(y)) \\cdot (\\mathrm{erase}\\ y\, f).prod\; g = f.prod g $$$$
Lean4
/-- Taking a product over `f : α →₀ M` is the same as multiplying the value on a single element
`y ∈ f.support` by the product over `erase y f`. -/
@[to_additive /-- Taking a sum over `f : α →₀ M` is the same as adding the value on a
single element `y ∈ f.support` to the sum over `erase y f`. -/
]
theorem mul_prod_erase (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y ∈ f.support) :
g y (f y) * (erase y f).prod g = f.prod g := by
classical
rw [Finsupp.prod, Finsupp.prod, ← Finset.mul_prod_erase _ _ hyf, Finsupp.support_erase, Finset.prod_congr rfl]
intro h hx
rw [Finsupp.erase_ne (ne_of_mem_erase hx)]
