Theorem LSeries.abscissaOfAbsConv_le_one_of_isBigO_one

Modification history

2025-01-30 15:01
Mathlib/NumberTheory/LSeries/Convergence.lean
chore(NumberTheory/LSeries): unsqueeze lots of terminal simps (#21133)
Modified LSeries.abscissaOfAbsConv_le_one_of_isBigO_oneView on Github →
2024-03-04 09:02
Mathlib/NumberTheory/LSeries/Convergence.lean
refactor(NumberTheory/LSeries/*): change type of argument to `ℕ → ℂ`, add `LSeries.term` + API etc. (#11111) …
Added LSeries.abscissaOfAbsConv_le_one_of_isBigO_oneView on Github →