Theorems · Definition · number theory
LSeries
(ℕ → ℂ) → ℂ → ℂ
The value of the L-series of the sequence f at the point s
if it converges absolutely there, and 0 otherwise.
- Defined in
- Mathlib.NumberTheory.LSeries.Basic
- Cited by
- 77 results in Mathlib
- Foundations
- Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- SummationFilter.unconditionalproof · cited by 2,068
- tsumproof · cited by 1,148
- LSeries.termproof · cited by 48
Cited by79
Results whose statement or proof uses this declaration.
- LSeries_congrstatement · cited by 9
- LSeries_one_eq_riemannZetastatement · cited by 6
- LSeriesSummable.LSeriesHasSumstatement · cited by 5
- LSeries_convolution'statement · cited by 5
- DirichletCharacter.LFunction_eq_LSeriesstatement · cited by 4
- DirichletCharacter.LSeries_eulerProduct_exp_logstatement · cited by 3
- ArithmeticFunction.LSeries_zeta_eqstatement · cited by 3
- LSeries.positivestatement · cited by 3
- LSeries_deltastatement · cited by 3
- LSeries_hasDerivAtstatement · cited by 3
- LSeries_zerostatement · cited by 3
- DirichletCharacter.LSeries_eulerProduct_hasProdstatement · cited by 2