Theorems · Theorem · number theory
LSeriesSummable.of_re_le_re
∀ {f : ℕ → ℂ} {s s' : ℂ}, s.re ≤ s'.re → LSeriesSummable f s → LSeriesSummable f s'- Defined in
- Mathlib.NumberTheory.LSeries.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Complex.restatement and proof · cited by 882
- norm_nonnegproof · cited by 725
- LSeriesSummablestatement and proof · cited by 59
- LSeries.termproof · cited by 48
- Summable.of_nonneg_of_leproof · cited by 36
- summable_norm_iffproof · cited by 8
- LSeries.norm_term_le_of_re_le_reproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- LSeriesSummable_of_abscissaOfAbsConv_lt_reproof · cited by 9
- LSeriesSummable.abscissaOfAbsConv_leproof · cited by 3
- DirichletCharacter.LSeriesSummable_iffproof · cited by 3
- ArithmeticFunction.LSeriesSummable_moebius_iffproof · cited by 2
- LSeriesSummable_iff_of_re_eq_reproof · cited by 0