Commit 2024-10-05 08:48 f1c9c723

View on Github →

feat: asymptotics lemmas (#17394) From https://github.com/MichaelStollBayreuth/EulerProducts

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.isBigO_mul_iff_isBigO_div

added theorem Asymptotics.isLittleO_id_one