bernoulli'_four

Mathlib.NumberTheory.Bernoulli

URI: https://scilib.ai/kg/mathlib#bernoulli'_four

← MathLib Explorer

English

The fourth Bernoulli' number equals minus one over thirty: B'(4) = -1/30.

Русский

Четвёртая Bernoulli' равна -1/30: B'(4) = -1/30.

LaTeX

$$$\text{bernoulli'}(4) = -\tfrac{1}{30}$$$

Lean4

@[simp]
theorem bernoulli'_four : bernoulli' 4 = -1 / 30 :=
  by
  have : Nat.choose 4 2 = 6 := by
    decide -- shrug

  rw [bernoulli'_def]
  norm_num [sum_range_succ, sum_range_succ, sum_range_zero, this]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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