Theorem Asymptotics.IsLittleO.add_iff_left

Modification history

2026-08-24 06:52
Mathlib/Analysis/Asymptotics/Arith.lean
refactor(Analysis/Asymptotics): split long file Defs.lean (#42997) …
Modified Asymptotics.IsLittleO.add_iff_leftView on Github →
2025-12-17 21:56
Mathlib/Analysis/Asymptotics/Defs.lean
chore(Analysis): fix whitespace (#32909) …
Modified Asymptotics.IsLittleO.add_iff_leftView on Github →
2025-03-21 07:31
Mathlib/Analysis/Asymptotics/Defs.lean
feat(Analysis/Asymptotics) `IsBigO.add_iff_left` and variants (#23059) …
Added Asymptotics.IsLittleO.add_iff_leftView on Github →