English
Let A be a family of homogeneous pieces indexed by ι with a graded monoid structure. For any index map fι : α → ι and any choice of homogeneous elements fA a ∈ A (fι a) for each a in a finite list l of α, the value of the graded product along l, viewed as an element of the ambient ring R, equals the ordinary product of the chosen elements in R. In particular, taking the dProd of l yields the same result as multiplying the corresponding A-values in R.
Русский
Пусть A — семейство однородных компонент, индексируемых по ι, образующее градуированную моноиду. Для любой отображения fι : α → ι и для каждого a из конечного списка l из α выбрать элемент fA a ∈ A (fι a). Значение градуированного произведения по списку l, рассматриваемое в окружающей кольцевой среде R, равно обычному произведению выбранных элементов в R. Специально, dProd(l, fι, fA) соответствует произведению элементов fA a в R.
LaTeX
$$$ \uparrow \big(\mathrm{List.dProd}(l, fι, fA)\big) = \mathrm{List.prod}(l.map(fA)) $$$$
Lean4
@[simp]
theorem coe_list_dProd (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) : R) := by
match l with
| [] => rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
| head :: tail => rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons, SetLike.coe_list_dProd _ _ _ tail]
