English
The Bernoulli' power series assigns to each A with a rational-algebra structure a formal power series whose nth coefficient is bernoulli'(n) under the algebra map from Q to A divided by n!.
Русский
Где A — кольцо, алгебра над Q, ряд Бернулли' задаётся так, что коэффициент при n-й степени равен bernoulli'(n) под картой алгебрации Q → A, делённой на n!.
LaTeX
$$$\text{bernoulli'PowerSeries} : (A) \to \text{PowerSeries } A, \quad \text{coeff}(n) = (\text{algebraMap } \mathbb{Q} A)(\bernoulli'(n) / n!)$$$
Lean4
/-- The exponential generating function for the Bernoulli numbers `bernoulli' n`. -/
def bernoulli'PowerSeries :=
mk fun n => algebraMap ℚ A (bernoulli' n / n !)