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 →