term_of_ne_zero

Mathlib.NumberTheory.LSeries.Basic

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

English

If n ≠ 0, then term f s n = f n / n^s.

Русский

Если n ≠ 0, то term f s n = f(n)/n^s.

LaTeX

$$$\\operatorname{term}(f,s,n) = \\dfrac{f(n)}{n^{s}}\\quad (n \\neq 0)$$$

Lean4

@[simp]
theorem term_of_ne_zero {n : ℕ} (hn : n ≠ 0) (f : ℕ → ℂ) (s : ℂ) : term f s n = f n / n ^ s :=
  if_neg hn

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

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

Разделы

Аффилиация

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