English
For A as above, the dProd of a list l, when viewed as an element of the subtype corresponding to the graded pieces, is exactly the pair whose first coordinate is the ordinary product ∏_{a∈l} fA a in R, together with a justification that this product lies in the appropriate graded piece A (∑_{a∈l} fι a).
Русский
Для A вышеупомянутой градации, dProd списка l как элемент подтипа соответствующих компонент равен паре, первая компонента которой равна обычному произведению ∏_{a∈l} fA a в R, вместе с доказательством принадлежности этого произведения нужной граде.
LaTeX
$$$ \mathrm{List.dProd}(l,fι,fA) = \langle \mathrm{List.prod}(l.map(fA)),\; (l.dProdIndex_eq_map_sum fι).symm \; \text{▸} \; \text{list_prod_map_mem_graded } l\ _ _ \text{(fun i _ => (fA i).prop)} \rangle $$$
Lean4
/-- A version of `List.coe_dProd_set_like` with `Subtype.mk`. -/
theorem list_dProd_eq (A : ι → S) [SetLike.GradedMonoid A] (fι : α → ι) (fA : ∀ a, A (fι a)) (l : List α) :
(@List.dProd _ _ (fun i => ↥(A i)) _ _ l fι fA) =
⟨List.prod (l.map fun a => fA a),
(l.dProdIndex_eq_map_sum fι).symm ▸ list_prod_map_mem_graded l _ _ fun i _ => (fA i).prop⟩ :=
Subtype.ext <| SetLike.coe_list_dProd _ _ _ _
