chudnovskyNum

Mathlib.Analysis.Real.Pi.Chudnovsky

URI: https://scilib.ai/kg/mathlib#chudnovskyNum

English

The numerator of the nth term in Chudnovsky's series for π is

Русский

Numerator чередующей последовательности Чудновского для π равен

LaTeX

$$$\\operatorname{chudnovskyNum}(n) = (-1)^n \\,(6n)!\\,(545140134\\,n + 13591409).$$$

Lean4

/-- The numerator of the nth term in Chudnovsky's series -/
def chudnovskyNum (n : ℕ) : ℤ :=
  (-1 : ℤ) ^ n * (6 * n)! * (545140134 * n + 13591409)

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

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

Разделы

Аффилиация

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