chudnovskyDenom

Mathlib.Analysis.Real.Pi.Chudnovsky

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

English

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

Русский

Знаменатель n-го члена ряда Чудновского для π

LaTeX

$$$\\operatorname{chudnovskyDenom}(n) = (3n)! \\cdot (n)!^3 \\cdot 640320^{3n}.$$$

Lean4

/-- The denominator of the nth term in Chudnovsky's series -/
def chudnovskyDenom (n : ℕ) : ℕ :=
  (3 * n)! * (n)! ^ 3 * 640320 ^ (3 * n)

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

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

Разделы

Аффилиация

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