Theorems · Theorem · ring theory

SetLike.list_dProd_eq

∀ {ι : Type u_1} {R : Type u_2} {α : Type u_3} {S : Type u_4} [inst : SetLike S R] [inst_1 : Monoid R]
  [inst_2 : AddMonoid ι] (A : ι → S) [inst_3 : SetLike.GradedMonoid A] (fι : α → ι) (fA : (a : α) → ↥(A (fι a)))
  (l : List α), l.dProd fι fA = ⟨(List.map (fun a => ↑(fA a)) l).prod, ⋯⟩

A version of List.coe_dProd_set_like with Subtype.mk.

Defined in

Mathlib.Algebra.GradedMonoid

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

SetLikeMonoidAddMonoidSetLike.GradedMonoid