Source indexedtheorem · leanprover/lean4:v4.32.0

Finset.sum_Icc_zero_eq_sum_Icc_one

PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation · PrimeNumberTheoremAnd/Mathlib/NumberTheory/AbelSummation.lean:47 to 58

Source documentation

If f 0 = 0, the term at 0 in Icc 0 N is redundant.

Exact Lean statement

theorem _root_.Finset.sum_Icc_zero_eq_sum_Icc_one {N : ℕ} {f : ℕ → 𝕜} (h0 : f 0 = 0) :
    ∑ k ∈ Icc 0 N, f k = ∑ k ∈ Icc 1 N, f k

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem _root_.Finset.sum_Icc_zero_eq_sum_Icc_one {N : ℕ} {f : ℕ → 𝕜} (h0 : f 0 = 0) :    ∑ k ∈ Icc 0 N, f k = ∑ k ∈ Icc 1 N, f k := by  have hdecomp : insert 0 (Icc 1 N) = Icc 0 N := by    simpa [Nat.succ_eq_add_one] using      insert_Icc_succ_left_eq_Icc (a := 0) (b := N) (h := Nat.zero_le N)  have hnotmem : (0 : ℕ) ∉ Icc 1 N := by    intro h    exact (not_le.mpr (Nat.lt_succ_self 0)) (mem_Icc.mp h).1  calc    ∑ k ∈ Icc 0 N, f k = ∑ k ∈ insert 0 (Icc 1 N), f k := by simp [hdecomp]    _ = f 0 + ∑ k ∈ Icc 1 N, f k := by simp    _ = ∑ k ∈ Icc 1 N, f k := by simp [h0]