Theorem: LSeries_eq_zero_of_abscissaOfAbsConv_eq_top (EulerProducts/LSeriesUnique.lean)

State before:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0
Tactic:
ext s
State after:
case h
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s

State before:
case h
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s
Tactic:
exact LSeries.eq_zero_of_not_LSeriesSummable f s <| mt LSeriesSummable.abscissaOfAbsConv_le <|
  h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false
State after:
no goals