Theorems · Theorem · number theory
bernoulliFourierCoeff_recurrence
∀ (k : ℕ) {n : ℤ},
n ≠ 0 →
bernoulliFourierCoeff k n =
1 / (-2 * ↑Real.pi * Complex.I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)Recurrence relation (in k) for the n-th Fourier coefficient of Bₖ.
- Defined in
- Mathlib.NumberTheory.ZetaValues
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 272 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites37
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realproof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Algebra.algebraMapproof · cited by 4,706
- one_mulproof · cited by 2,841
- HasQuotient.Quotientproof · cited by 2,301
- Real.pistatement and proof · cited by 1,774
- Complex.ofRealstatement and proof · cited by 1,654
- sub_zeroproof · cited by 938
- Complex.Istatement and proof · cited by 866
- Polynomial.mapproof · cited by 806
- zero_lt_oneproof · cited by 598
Cited by2
Results whose statement or proof uses this declaration.
- bernoulli_zero_fourier_coeffproof · cited by 1
- bernoulliFourierCoeff_eqproof · cited by 1