Finset.sum to double sum

Stream: new members

[Junjie Bai]

Is there any function can transform Finset.sum to a double sum? I got a group G, there is a filtration of normal subgroup on G, denoted G_i, and I want to realize that :

∑ x in G, f x = ∑ i in Finset.Icc 0 u, ∑ x in G_i / G_(i + 1), f x + ∑ x in G_u ,f x

[Yaël Dillies]

docs#Finset.sum_product

[Yaël Dillies]

Given how you want to use, docs#Finset.sum_product' will probably be more useful

[Junjie Bai]

That helps, thank you!