## Stream: new members

### Topic: big_operator not starting from zero

#### Horatiu Cheval (Aug 22 2021 at 13:58):

What would be the recommended way, with best API, for writing a big operator over a range not starting from zero, like $\prod_{i = n}^{n + m} a_i$?
I can think of two options:

∏ i in range (m + 1), a (n + i)


or

∏ i in (range (n + m + 1)).filter (nat.le n), a i


Is one better supported than the other, or maybe there's some other standard option?

#### Ruben Van de Velde (Aug 22 2021 at 14:05):

Without much experience to cloud my judgment, I'd probably pick the first option :)

#### Horatiu Cheval (Aug 22 2021 at 14:36):

That's what I tried at first too. But then how do I go about decomposing it into products starting from zero, i.e. $\prod_{i=0}^m a_{n + i} \cdot \prod_{i = 0}^{n-1} a_i = \prod_{i=0}^{n+m} a_i$?

#### Horatiu Cheval (Aug 22 2021 at 14:39):

This seemed not hard to do (haven't tried yet) in the second variant with some results about products over unions of finsets, which exist in mathlib

#### Eric Wieser (Aug 22 2021 at 15:18):

We already have that lemma somewhere

#### Eric Wieser (Aug 22 2021 at 15:18):

docs#finset.prod_range_add, guessed by what the statement would be

#### Horatiu Cheval (Aug 22 2021 at 17:34):

That's great, thank you!

#### Bolton Bailey (Aug 23 2021 at 09:45):

For your additional reference there is also docs#finset.Ico, which represents more directly an interval of naturals. You may have more luck working with range, depending on what lemmas you want to use.

Last updated: Dec 20 2023 at 11:08 UTC