bernoulliPowerSeries — Mathlib

English

The Bernoulli numbers generate an exponential generating function in A: the power series whose nth coefficient is B_n/n! mapped from ℚ to A.

Русский

Числа Бернулли задают экспоненциальную порождающую функцию; это Степенной ряд, где коэффициент при X^n равен B_n/n!, приводимый в A через алгебраическое отображение ℚ → A.

LaTeX

$$$\text{bernoulliPowerSeries}(A) = \text{PowerSeries.mk}(n \mapsto \text{algebraMap}_{\mathbb{Q} \to A}(\text{bernoulli}(n)/n!))$$$

Lean4

/-- The exponential generating function for the Bernoulli numbers `bernoulli n`. -/
def bernoulliPowerSeries :=
  mk fun n => algebraMap ℚ A (bernoulli n / n !)

Похожие утверждения