Theorems · Theorem · number theory

tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α]
  {f : ℕ → α},
  Summable f →
    Function.support f ⊆ {n | IsPrimePow n} →
      ∑' (n : ℕ), f n = ∑' (p : Nat.Primes), f ↑p + ∑' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))

Defined in

Mathlib.NumberTheory.EulerProduct.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupUniformSpaceIsUniformAddGroupCompleteSpaceT0Space