coercion over Finset summing?

Stream: Is there code for X?

[Alex Kontorovich]

Is there a way to easily convert between summing over ℤ and over ℕ? E.g.:

import Mathlib

open BigOperators

lemma Finset_coe_Nat_Int (f : ℤ → ℂ) (m n : ℕ) :
    (∑ x in Finset.Ioc m n, f x) = ∑ x in Finset.Ioc (m : ℤ) n, f x := by
  sorry

Thanks!

[Daniel Weber]

You should be able to use docs#Finset.sum_nbij' (or perhaps docs#Finset.sum_nbij would be easier) fairly easily, I'm not sure if there's an easier way

[Yaël Dillies]

No, don't use sum_bij (or friends) here! That's overkill

[Yaël Dillies]

What you usually want to use in such a situation is docs#Finset.sum_map

[Yaël Dillies]

For this, you will need a version of docs#Nat.image_cast_int_Ioc stated using docs#Finset.map. That should be very easy to do

[Alex Kontorovich]

Oh. I already did it...

[Yaël Dillies]

Well, at least you now know what the mathlib PR should look like :smile: