Theorems · Definition · ring theory
List.dProdIndex
{ι : Type u_1} → {α : Type u_2} → [AddMonoid ι] → List α → (α → ι) → ιThe index used by List.dProd. Propositionally this is equal to (l.map fι).Sum, but
definitionally it needs to have a different form to avoid introducing Eq.recs in List.dProd.
- Defined in
- Mathlib.Algebra.GradedMonoid
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- AddMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
Cited by13
Results whose statement or proof uses this declaration.
- List.dProdstatement · cited by 10
- GradedMonoid.mk_list_dProdstatement · cited by 2
- SetLike.coe_list_dProdstatement · cited by 1
- DirectSum.list_prod_ofFn_of_eq_dProdstatement and proof · cited by 1
- DirectSum.ofList_dProdstatement and proof · cited by 1
- List.dProdIndex_eq_map_sumstatement · cited by 1
- GradedMonoid.list_prod_map_eq_dProdstatement · cited by 1
- SetLike.list_dProd_eqstatement · cited by 0
- List.dProdIndex_consstatement · cited by 0
- List.dProdIndex_nilstatement · cited by 0
- List.dProd_consstatement · cited by 0
- GradedMonoid.list_prod_ofFn_eq_dProdstatement and proof · cited by 0