Theorems · Theorem · number theory
summable_bernoulli_fourier
∀ {k : ℕ}, 2 ≤ k → Summable fun n => -↑k.factorial / (2 * ↑Real.pi * Complex.I * ↑n) ^ k- Defined in
- Mathlib.NumberTheory.ZetaValues
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement and proof · cited by 5,565
- Norm.normproof · cited by 5,413
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- absproof · cited by 1,814
- Real.pistatement and proof · cited by 1,774
- Complex.ofRealstatement and proof · cited by 1,654
- Complex.Istatement and proof · cited by 866
- Summablestatement and proof · cited by 778
- one_divproof · cited by 624
- Nat.factorialstatement and proof · cited by 616
- mul_powproof · cited by 220
- norm_invproof · cited by 126
Cited by1
Results whose statement or proof uses this declaration.
- hasSum_one_div_pow_mul_fourier_mul_bernoulliFunproof · cited by 1