Theorems · Theorem · number theory

Nat.sumByResidueClasses

∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : UniformSpace R] [IsUniformAddGroup R] [CompleteSpace R] [T0Space R]
  {f : ℕ → R}, Summable f → ∀ (N : ℕ) [inst_5 : NeZero N], ∑' (n : ℕ), f n = ∑ j, ∑' (m : ℕ), f (j.val + N * m)

If f is a summable function on ℕ, and 0 < N, then we may compute ∑' n : ℕ, f n by summing each residue class mod N separately.

Defined in

Mathlib.Analysis.SumOverResidueClass

Cited by

1 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupUniformSpaceIsUniformAddGroupCompleteSpaceT0SpaceNeZero