Theorems · Theorem · number theory

Polynomial.bernoulli_generating_function

∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] (t : A),
  (PowerSeries.mk fun n => (Polynomial.aeval t) ((1 / ↑n.factorial) • Polynomial.bernoulli n)) *
      (PowerSeries.exp A - 1) =
    PowerSeries.X * (PowerSeries.rescale t) (PowerSeries.exp A)

The theorem that $(e^X - 1) * ∑ Bₙ(t)* X^n/n! = Xe^{tX}$

Defined in

Mathlib.NumberTheory.BernoulliPolynomials

Cited by

0 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAlgebra