Theorem Asymptotics.IsBigOWith.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.IsBigOWith.sum_congrView on Github →