logTaylor_zero

Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

URI: https://scilib.ai/kg/mathlib#Complex.logTaylor_zero

English

The 0-th Taylor polynomial of log is the zero function.

Русский

Нулевой полином Тейлора логарифма есть нулевая функция.

LaTeX

$$$\logTaylor(0) = 0$$$

Lean4

theorem logTaylor_zero : logTaylor 0 = fun _ ↦ 0 := by
  funext
  simp only [logTaylor, Finset.range_zero, Finset.sum_empty]

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

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

Разделы

Аффилиация

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