Theorems · Theorem · number theory
bernoulliFun_eq_integral
∀ (k : ℕ) (x y : ℝ), bernoulliFun (k + 1) y = bernoulliFun (k + 1) x + ∫ (t : ℝ) in x..y, ↑(k + 1) * bernoulliFun k t
Fundamental theorem of calculus to express a Bernoulli polynomial via the previous one
- Defined in
- Mathlib.NumberTheory.ZetaValues
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 268 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasureTheory.MeasureSpace.volumestatement · cited by 1,323
- intervalIntegralstatement · cited by 546
- Set.uIccproof · cited by 393
- add_sub_cancelproof · cited by 195
- Continuous.comp'proof · cited by 184
- continuous_const_mulproof · cited by 47
- Continuous.intervalIntegrableproof · cited by 32
- bernoulliFunstatement and proof · cited by 27
- intervalIntegral.integral_eq_sub_of_hasDerivAtproof · cited by 11
- hasDerivAt_bernoulliFunproof · cited by 5
- continuous_bernoulliFunproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.