range(n,m)

Stream: Is there code for X?

[Rémy Degenne]

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]

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

[Eric Wieser]

docs#set.Ico?

[Rémy Degenne]

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

[Rémy Degenne]

my lemma above looks similar to finset.prod_Ico_eq_prod_range

[Rémy Degenne]

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]

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.