bernoulli'_zero

Mathlib.NumberTheory.Bernoulli

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

English

The modified Bernoulli numbers satisfy B'(0) = 1.

Русский

Пусть B' обозначает модифицированные числа Бернулли; тогда B'(0) = 1.

LaTeX

$$$\text{bernoulli'}(0) = 1$$$

Lean4

@[simp]
theorem bernoulli'_zero : bernoulli' 0 = 1 := by
  rw [bernoulli'_def]
  simp

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

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

Разделы

Аффилиация

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