Theorems · Theorem · number theory
tsum_primes_pow_eq
∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α]
{f : ℕ → α},
(Summable fun n => f ↑n) → ∑' (p : Nat.Primes) (n : ℕ), f (↑p ^ (n + 1)) = ∑' (n : { n // IsPrimePow n }), f ↑n- Defined in
- Mathlib.NumberTheory.EulerProduct.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- AddCommGroupstatement and proof · cited by 12,871
- CompleteSpacestatement and proof · cited by 2,532
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- Nat.Primestatement · cited by 2,059
- UniformSpacestatement and proof · cited by 2,040
- tsumstatement and proof · cited by 1,148
- Summablestatement and proof · cited by 778
- Equiv.injectiveproof · cited by 464
- IsUniformAddGroupstatement and proof · cited by 342
- T0Spacestatement and proof · cited by 179
- IsPrimePowstatement and proof · cited by 77
Cited by2
Results whose statement or proof uses this declaration.
- DirichletCharacter.eulerProduct_log_eq_LSeriesproof · cited by 1
- tsum_eq_tsum_primes_of_support_subset_prime_powersproof · cited by 1