Theorem Asymptotics.isLittleO_id_iff_tendsto

Modification history

2026-11-11 18:16
Mathlib/Analysis/Asymptotics/Lemmas.lean
feat(NumberTheory/LSeries): the (weak) prime number theorem (#43238) …
Added Asymptotics.isLittleO_id_iff_tendstoView on Github →