English
A generalized version: if ∀ i, g i 0 = 1, then g(y,f(y)) · (erase y f).prod g = f.prod g whether or not y ∈ support(f).
Русский
Обобщенная версия: если ∀ i, g i 0 = 1, тогда независимо от того, принадлежит ли y поддержке f, выполняется равенство: g(y,f(y)) · (erase y f).prod g = f.prod g.
LaTeX
$$$$ \\forall i, g_i(0)=1 \\Rightarrow g(y,f(y)) \\cdot (\\mathrm{erase}\\ y\, f).prod g = f.prod g $$$$
Lean4
/-- Generalization of `Finsupp.mul_prod_erase`: if `g` maps a second argument of 0 to 1,
then its product over `f : α →₀ M` is the same as multiplying the value on any element
`y : α` by the product over `erase y f`. -/
@[to_additive /-- Generalization of `Finsupp.add_sum_erase`: if `g` maps a second argument of 0
to 0, then its sum over `f : α →₀ M` is the same as adding the value on any element
`y : α` to the sum over `erase y f`. -/
]
theorem mul_prod_erase' (f : α →₀ M) (y : α) (g : α → M → N) (hg : ∀ i : α, g i 0 = 1) :
g y (f y) * (erase y f).prod g = f.prod g := by
classical
by_cases hyf : y ∈ f.support
· exact Finsupp.mul_prod_erase f y g hyf
· rw [notMem_support_iff.mp hyf, hg y, erase_of_notMem_support hyf, one_mul]
