Theorems · Theorem · number theory

Nat.Primes.hasSum_iff_hasSum_ite

∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] (f : ℕ → M) {a : M},
  HasSum (fun p => f ↑p) a ↔ HasSum (fun n => if Nat.Prime n then f n else 0) a

HasSum over Nat.Primes iff over ℕ extending f by 0.

Defined in

Mathlib.NumberTheory.SumPrimeReciprocals

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpace