pow_mul_term_eq

Mathlib.NumberTheory.LSeries.Basic

URI: https://scilib.ai/kg/mathlib#LSeries.pow_mul_term_eq

← MathLib Explorer

English

For any f, s, n, (n+1)^s · term f s (n+1) = f(n+1).

Русский

Для любых f, s, n выполняется (n+1)^s · term f s (n+1) = f(n+1).

LaTeX

$$$(n+1)^{s} \\cdot \\operatorname{term}(f,s,n+1) = f(n+1)$$$

Lean4

theorem pow_mul_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : (n + 1) ^ s * term f s (n + 1) = f (n + 1) := by
  simp [term, natCast_add_one_cpow_ne_zero n _, mul_div_assoc']

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

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

Разделы

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

Аффилиация

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