English
Under suitable h:β → M → N with normalization h b 0 = 1 and h b (m1+m2) = h b m1 h b m2, the finsupp.mapDomain f s prod h equals s.prod (λ a m, h (f a) m).
Русский
При заданных условиях нормализации h на каждом b, произведение after mapDomain совпадает с исходным произведением после замены аргумента по f.
LaTeX
$$$(\\operatorname{mapDomain} f s).\\text{prod} h = s.\\text{prod} (\\lambda a m, h (f a) m).$$$
Lean4
@[to_additive]
theorem prod_mapDomain_index [CommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (h_zero : ∀ b, h b 0 = 1)
(h_add : ∀ b m₁ m₂, h b (m₁ + m₂) = h b m₁ * h b m₂) : (mapDomain f s).prod h = s.prod fun a m => h (f a) m :=
(prod_sum_index h_zero h_add).trans <|
prod_congr fun _ _ =>
prod_single_index
(h_zero _)
-- Note that in `prod_mapDomain_index`, `M` is still an additive monoid,
-- so there is no analogous version in terms of `MonoidHom`.
