Sums/products over integer intervals

This file contains some lemmas about sums and products over integer intervals Ixx.

theorem Finset.prod_Icc_of_even_eq_range {α : Type u_1} [CommGroup α] {f : ℤ → α} (hf : Function.Even f) (N : ℕ) : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0

theorem Finset.sum_Icc_of_even_eq_range {α : Type u_1} [AddCommGroup α] {f : ℤ → α} (hf : Function.Even f) (N : ℕ) : ∑ m ∈ Icc (-↑N) ↑N, f m = 2 • ∑ m ∈ range (N + 1), f ↑m - f 0

theorem Finset.prod_Icc_eq_prod_Ico_mul {α : Type u_1} [CommMonoid α] (f : ℤ → α) {l u : ℤ} (h : l ≤ u) : ∏ m ∈ Icc l u, f m = (∏ m ∈ Ico l u, f m) * f u

theorem Finset.sum_Icc_eq_sum_Ico_add {α : Type u_1} [AddCommMonoid α] (f : ℤ → α) {l u : ℤ} (h : l ≤ u) : ∑ m ∈ Icc l u, f m = ∑ m ∈ Ico l u, f m + f u

theorem Finset.prod_Icc_succ_eq_mul_endpoints {R : Type u_1} [CommGroup R] (f : ℤ → R) {N : ℕ} : ∏ m ∈ Icc (-(↑N + 1)) (↑N + 1), f m = f (↑N + 1) * f (-(↑N + 1)) * ∏ m ∈ Icc (-↑N) ↑N, f m

theorem Finset.sum_Icc_succ_eq_add_endpoints {R : Type u_1} [AddCommGroup R] (f : ℤ → R) {N : ℕ} : ∑ m ∈ Icc (-(↑N + 1)) (↑N + 1), f m = f (↑N + 1) + f (-(↑N + 1)) + ∑ m ∈ Icc (-↑N) ↑N, f m

theorem Finset.prod_Ico_int_div (b : ℕ) {α : Type u_1} [CommGroup α] (f : ℤ → α) : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b

theorem Finset.sum_Ico_int_sub (b : ℕ) {α : Type u_1} [AddCommGroup α] (f : ℤ → α) : ∑ n ∈ Ico (-↑b) ↑b, (f n - f (n + 1)) = f (-↑b) - f ↑b