English
A variant rewriting the other way: the product of a mapped list equals a single mk of the corresponding dProd.
Русский
Вариант, позволяющий переписать в обратном направлении: произведение отображенного списка равно одному mk, соответствующему dProd.
LaTeX
$$$(\\mathrm{List.map}\ f\ l).\\mathrm{prod} = \\mathrm{GradedMonoid.mk} \\(l.dProdIndex (\\lambda i. (f i).fst)\\) \\(l.dProd (\\lambda i. (f i).fst) (\\lambda i. (f i).snd) \\)$$$
Lean4
/-- A variant of `GradedMonoid.mk_list_dProd` for rewriting in the other direction. -/
theorem list_prod_map_eq_dProd (l : List α) (f : α → GradedMonoid A) :
(l.map f).prod = GradedMonoid.mk _ (l.dProd (fun i => (f i).1) fun i => (f i).2) :=
by
rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]
simp_rw [Sigma.eta]
