Theorems · Definition · ring theory

List.dProd

{ι : Type u_1} →
  {α : Type u_2} →
    {A : ι → Type u_3} →
      [inst : AddMonoid ι] →
        [GradedMonoid.GMonoid A] → (l : List α) → (fι : α → ι) → ((a : α) → A (fι a)) → A (l.dProdIndex fι)

A dependent product for graded monoids represented by the indexed family of types A i. This is a dependent version of (l.map fA).prod. For a list l : List α, this computes the product of fA a over a, where each fA is of type A (fι a).

Defined in

Mathlib.Algebra.GradedMonoid

Cited by

10 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

AddMonoidGradedMonoid.GMonoid