# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: range(n,m)

#### Rémy Degenne (Dec 11 2020 at 10:22):

I just wrote several lemmas involving sums and products over `finset.range(m)\finset.range(n)`

and now I am thinking that maybe those exist somewhere. Is there a type for the natural numbers j verifying n <= j < m? Even if there is no such type, is there a file with lemmas like the following:

```
lemma prod_range_sdiff_offset {α} [comm_monoid α] (N r : ℕ) (f : ℕ → α) :
(∏ (n : ℕ) in (finset.range (N + r) \ finset.range N), f n)
= ∏ (n : ℕ) in finset.range (r), f (N + n) := sorry
```

#### Eric Wieser (Dec 11 2020 at 10:24):

docs#list.range', perhaps? I guess that's not quite there either

#### Eric Wieser (Dec 11 2020 at 10:25):

#### Rémy Degenne (Dec 11 2020 at 10:34):

Thanks for giving me the Ico idea : I just found algebra.big_operators.intervals

#### Rémy Degenne (Dec 11 2020 at 10:34):

my lemma above looks similar to `finset.prod_Ico_eq_prod_range`

#### Rémy Degenne (Dec 11 2020 at 10:36):

and apparently there is a `finset.Ico`

. The finset part of mathlib really is the scary part to me. it feels like there are 100 different types and that making them interact is not that easy

#### Kevin Buzzard (Dec 11 2020 at 13:17):

I have been worrying on and off about these lemmas for $\sum_{i=a}^b$ for years now, and my current gut feeling is that `finset.Ico`

works great and summing/prodding over that finset should be the default way to express stuff.

Last updated: May 17 2021 at 15:13 UTC