Theorems · Theorem · number theory

LSeries.eq_of_LSeries_eventually_eq

∀ {f g : ℕ → ℂ},
  LSeries.abscissaOfAbsConv f < ⊤ →
    LSeries.abscissaOfAbsConv g < ⊤ →
      ((fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x) → ∀ {n : ℕ}, n ≠ 0 → f n = g n

If the LSeries of f and of g converge somewhere and agree on large real arguments, then f n = g n whenever n ≠ 0.

Defined in: Mathlib.NumberTheory.LSeries.Injectivity
Cited by: 1 results in Mathlib
Foundations: Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Top.topstatement and proof · cited by 9,680
Complexstatement and proof · cited by 5,565
Filter.atTopstatement and proof · cited by 2,405
Filter.EventuallyEqstatement and proof · cited by 1,912
Complex.ofRealstatement and proof · cited by 1,654
LE.le.trans_ltproof · cited by 795
ERealstatement · cited by 793
lt_top_iff_ne_topproof · cited by 95
LSeriesstatement and proof · cited by 77
LSeries.abscissaOfAbsConvstatement and proof · cited by 50
max_ltproof · cited by 42

Cited by1

Results whose statement or proof uses this declaration.

LSeries_eq_iff_of_abscissaOfAbsConv_lt_topproof · cited by 1