ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ List.prod (List.map r (List.finRange n)) ∈ A (List.sum (List.map i (List.finRange n)))
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ List.prod (List.ofFn r) ∈ A (List.sum (List.ofFn i))
rw [List.ofFn_eq_map, List.ofFn_eq_map]
no goals
ι : Type u_3
R : Type u_1
S : Type u_2
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ List.prod (List.map r (List.finRange n)) ∈ A (List.sum (List.map i (List.finRange n)))
exact list_prod_map_mem_graded _ _ _ fun _ _ => h _