Theorem Asymptotics.IsBigOWith.sum_congr

Modification history

2026-08-24 06:52
Mathlib/Analysis/Asymptotics/Arith.lean
refactor(Analysis/Asymptotics): split long file Defs.lean (#42997) …
Modified Asymptotics.IsBigOWith.sum_congrView on Github →
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 →