Commit 2025-12-07 22:48 a2c6b11a

View on Github →

feat(Analysis/Asymptotics): Variants of isBigO_mul_iff_isBigO_div (#32544) Modifies the proof of isBigO_mul_iff_isBigO_div to first prove for IsBigOWith. This is then used to prove a version for IsLittleO.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

added theorem Asymptotics.isBigOWith_mul_iff_isBigOWith_div

added theorem Asymptotics.isLittleO_mul_iff_isLittleO_div