logTaylor_at_zero

Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

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

← MathLib Explorer

English

For every n, evaluating logTaylor n at 0 gives 0.

Русский

Для каждого n значение logTaylor n в 0 равно 0.

LaTeX

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

Lean4

theorem logTaylor_at_zero (n : ℕ) : logTaylor n 0 = 0 := by
  induction n with
  | zero => simp [logTaylor_zero]
  | succ n ih => simpa [logTaylor_succ, ih] using ne_or_eq n 0

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

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

Разделы

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

Аффилиация

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