Theorems · Theorem · ring theory

GradedMonoid.list_prod_map_eq_dProd

∀ {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] (l : List α)
  (f : α → GradedMonoid A),
  (List.map f l).prod =
    GradedMonoid.mk (l.dProdIndex fun i => (f i).fst) (l.dProd (fun i => (f i).fst) fun i => (f i).snd)

A variant of GradedMonoid.mk_list_dProd for rewriting in the other direction.

Defined in: Mathlib.Algebra.GradedMonoid
Cited by: 1 results in Mathlib
Foundations: Depth 12 from the axioms · uses propext, Quot.sound
Assumes: AddMonoid GradedMonoid.GMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

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
GradedMonoidstatement and proof · cited by 46
GradedMonoid.mkstatement · cited by 27
Sigma.etaproof · cited by 25
GradedMonoid.GMonoidstatement and proof · cited by 24
List.dProdIndexstatement · cited by 12
List.dProdstatement · cited by 10
GradedMonoid.mk_list_dProdproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

GradedMonoid.list_prod_ofFn_eq_dProdproof · cited by 0