Mathlib Map

Theorems · Definition · number theory

LSeries.term

(ℕ → ℂ) → ℂ → ℕ → ℂ

The nth term of the L-series of f evaluated at s. We set it to zero when n = 0.

Defined in
Mathlib.NumberTheory.LSeries.Basic
Cited by
48 results in Mathlib
Foundations
Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Complexstatement and proof · cited by 5,565

Cited by51

Results whose statement or proof uses this declaration.