## 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

#### 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