English
Taking the product over a sum of finsupps distributes as a product of individual products, given suitable h a_0 and h_add conditions.
Русский
Произведение над суммой финспп распадается на произведения по каждому члену, при наличии условий на h_0 и h_add.
LaTeX
$$$$ (f+g).prod h = f.prod h \cdot g.prod h \quad\text{provided } h_0 \text{ and } h_{add} \text{ hold}. $$$$
Lean4
/-- Taking the product under `h` is an additive-to-multiplicative homomorphism of finsupps,
if `h` is an additive-to-multiplicative homomorphism on the support.
This is a more general version of `Finsupp.prod_add_index'`; the latter has simpler hypotheses. -/
@[to_additive /-- Taking the product under `h` is an additive homomorphism of finsupps, if `h` is an
additive homomorphism on the support. This is a more general version of
`Finsupp.sum_add_index'`; the latter has simpler hypotheses. -/
]
theorem prod_add_index [DecidableEq α] [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N}
(h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1)
(h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂), h a (b₁ + b₂) = h a b₁ * h a b₂) :
(f + g).prod h = f.prod h * g.prod h :=
by
rw [Finsupp.prod_of_support_subset f subset_union_left h h_zero,
Finsupp.prod_of_support_subset g subset_union_right h h_zero, ← Finset.prod_mul_distrib,
Finsupp.prod_of_support_subset (f + g) Finsupp.support_add h h_zero]
exact Finset.prod_congr rfl fun x hx => by apply h_add x hx
