coeff_exp

Mathlib.RingTheory.PowerSeries.WellKnown

URI: https://scilib.ai/kg/mathlib#PowerSeries.coeff_exp

English

For any nonzero A over ℚ, the nth coefficient of exp A equals algebraMap ℚ A (1/n!).

Русский

Коэффициент при X^n у экспоненты exp A равен алгебраическому отображению 1/n! из ℚ в A.

LaTeX

$$$$ \text{coeff}_n(\exp A) = \mathsf{algebraMap}_{\mathbb{Q} \to A}\left(\frac{1}{n!}\right) $$$$

Lean4

@[simp]
theorem coeff_exp : coeff n (exp A) = algebraMap ℚ A (1 / n !) :=
  coeff_mk _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru