bernoulli'_eq_bernoulli

Mathlib.NumberTheory.Bernoulli

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

English

The Bernoulli' numbers relate to the classical Bernoulli numbers by B'(n) = (-1)^n B(n).

Русский

Числа Бернулли' связаны с классическими числами Бернулли: B'(n) = (-1)^n B(n).

LaTeX

$$$\bernoulli'(n) = (-1)^n \cdot \bernoulli(n)$$$

Lean4

theorem bernoulli'_eq_bernoulli (n : ℕ) : bernoulli' n = (-1) ^ n * bernoulli n := by
  simp [bernoulli, ← mul_assoc, ← sq, ← pow_mul, mul_comm n 2]

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

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

Разделы

Аффилиация

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