term_of_ne_zero' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `s ≠ 0`, then the `if .. then .. else` construction in `LSeries.term` isn't needed, since
`0 ^ s = 0`.
-/
theorem term_of_ne_zero' {s : ℂ} (hs : s ≠ 0) (f : ℕ → ℂ) (n : ℕ) : term f s n = f n / n ^ s :=
  by
  rcases eq_or_ne n 0 with rfl | hn
  · rw [term_zero, Nat.cast_zero, zero_cpow hs, div_zero]
  · rw [term_of_ne_zero hn]

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