Theorems · Theorem · number theory

summable_indicator_mod_iff_summable_indicator_mod

∀ {m : ℕ} [NeZero m] {f : ℕ → ℝ},
  Antitone f → ∀ {k : ZMod m} (l : ZMod m), Summable ({n | ↑n = k}.indicator f) → Summable ({n | ↑n = l}.indicator f)

If a decreasing sequence of real numbers is summable on one residue class modulo m, then it is also summable on every other residue class mod m.

Defined in

Mathlib.Analysis.SumOverResidueClass

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZero