Theorems · Theorem · number theory
LSeries.abscissaOfAbsConv_one
LSeries.abscissaOfAbsConv 1 = 1
The abscissa of (absolute) convergence of the constant sequence 1 is 1.
- Defined in
- Mathlib.NumberTheory.LSeries.Dirichlet
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement · cited by 5,565
- one_ne_zeroproof · cited by 885
- ERealstatement · cited by 793
- LSeries.abscissaOfAbsConvstatement · cited by 50
- DirichletCharacter.modOne_eq_oneproof · cited by 4
- DirichletCharacter.absicssaOfAbsConv_eq_oneproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- riemannZeta_pos_of_one_ltproof · cited by 2
- ArithmeticFunction.LSeriesSummable_vonMangoldtproof · cited by 2
- ArithmeticFunction.abscissaOfAbsConv_zetaproof · cited by 0