chudnovskyTerm

Mathlib.Analysis.Real.Pi.Chudnovsky

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

English

The nth term of Chudnovsky's series for π⁻¹ is

Русский

n-й член ряда Чудновского для π⁻¹

LaTeX

$$$\\operatorname{chudnovskyTerm}(n) = \\frac{\\operatorname{chudnovskyNum}(n)}{\\operatorname{chudnovskyDenom}(n)}.$$$

Lean4

/-- The term at index `n` in Chudnovsky's series for `π⁻¹` -/
def chudnovskyTerm (n : ℕ) : ℚ :=
  chudnovskyNum n / chudnovskyDenom n

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

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

Разделы

Аффилиация

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