Theorems · Theorem · ring theory

SetLike.list_prod_map_mem_graded

∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  {A : ι → S} [SetLike.GradedMonoid A] {ι' : Type u_4} (l : List ι') (i : ι' → ι) (r : ι' → R),
  (∀ j ∈ l, r j ∈ A (i j)) → (List.map r l).prod ∈ A (List.map i l).sum

Defined in

Mathlib.Algebra.GradedMonoid

Cited by

2 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

SetLikeMonoidAddMonoidSetLike.GradedMonoid