Theorem Asymptotics.IsLittleO.sum_congr'

Modification history

2026-03-17 19:12
Mathlib/Analysis/Asymptotics/Defs.lean
feat(Mathlib/Analysis/Asymptotics/Defs): congr lemmas for IsBigO* (#35745) …
Added Asymptotics.IsLittleO.sum_congr'View on Github →