Theorems · Theorem · number theory
LSeriesSummable_congr
∀ {f g : ℕ → ℂ} (s : ℂ), (∀ {n : ℕ}, n ≠ 0 → f n = g n) → (LSeriesSummable f s ↔ LSeriesSummable g s)- Defined in
- Mathlib.NumberTheory.LSeries.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 194 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
- LSeriesSummablestatement · cited by 59
- summable_congrproof · cited by 2
- LSeries.term_congrproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- ArithmeticFunction.LSeriesSummable_zeta_iffproof · cited by 3
- LSeries.abscissaOfAbsConv_congrproof · cited by 3
- LSeriesHasSum_congrproof · cited by 0