bernoulli'PowerSeries — Mathlib

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 !)

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