English
For any l, fι, fA, GradedMonoid.mk applied to the dProd equals the product of the mapped mk's.
Русский
Для списка l, отображения fι и fA произведение mk по списку эквивалентно произведению элементов mk, полученных из fι и fA.
LaTeX
$$$\\mathrm{GradedMonoid.mk}\\(l.dProd fι fA) = \\left(\\prod_{a\\in l} \\mathrm{GradedMonoid.mk}(fι a)(fA a)\\right)$$$
Lean4
theorem mk_list_dProd (l : List α) (fι : α → ι) (fA : ∀ a, A (fι a)) :
GradedMonoid.mk _ (l.dProd fι fA) = (l.map fun a => GradedMonoid.mk (fι a) (fA a)).prod := by
match l with
| [] => simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]; rfl
| head :: tail => simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
