Theorems · Theorem · number theory
fourierCoeff_bernoulli_eq
∀ {k : ℕ},
k ≠ 0 →
∀ (n : ℤ),
fourierCoeff (Complex.ofReal ∘ periodizedBernoulli k) n = -↑k.factorial / (2 * ↑Real.pi * Complex.I * ↑n) ^ k- Defined in
- Mathlib.NumberTheory.ZetaValues
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 275 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement and proof · cited by 5,565
- zero_addproof · cited by 2,366
- Real.pistatement and proof · cited by 1,774
- Complex.ofRealstatement and proof · cited by 1,654
- Complex.Istatement and proof · cited by 866
- Nat.factorialstatement and proof · cited by 616
- Fact.outproof · cited by 328
- UnitAddCirclestatement and proof · cited by 157
- lt_add_of_pos_rightproof · cited by 51
- bernoulliFunproof · cited by 27
- fourierCoeffstatement and proof · cited by 26
Cited by1
Results whose statement or proof uses this declaration.
- hasSum_one_div_pow_mul_fourier_mul_bernoulliFunproof · cited by 1