big_operator not starting from zero

Stream: new members

[Horatiu Cheval]

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]

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

[Horatiu Cheval]

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]

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]

We already have that lemma somewhere

[Eric Wieser]

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

[Horatiu Cheval]

That's great, thank you!

[Bolton Bailey]

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.