Theorems · Definition · number theory
DirichletCharacter.LFunctionTrivChar
(N : ℕ) → [NeZero N] → ℂ → ℂ
The L-function of the trivial character mod N.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 306 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NeZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement · cited by 5,565
- DirichletCharacter.LFunctionproof · cited by 23
Cited by12
Results whose statement or proof uses this declaration.
- DirichletCharacter.LFunctionTrivChar₁proof · cited by 7
- DirichletCharacter.LFunctionTrivChar_residue_onestatement and proof · cited by 2
- ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAuxproof · cited by 2
- DirichletCharacter.LFunctionTrivChar₁_apply_one_ne_zeroproof · cited by 1
- DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_onestatement and proof · cited by 1
- DirichletCharacter.differentiable_LFunctionTrivChar₁proof · cited by 1
- DirichletCharacter.LFunctionTrivChar_eq_mul_riemannZetastatement and proof · cited by 1
- ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux'proof · cited by 1
- DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁statement and proof · cited by 1
- DirichletCharacter.norm_LFunction_product_ge_onestatement and proof · cited by 0
- DirichletCharacter.LFunctionTrivChar.congr_simpstatement and proof · cited by 0
- DirichletCharacter.LFunctionTrivChar_isBigO_near_one_horizontalstatement and proof · cited by 0