Theorem Asymptotics.IsBigO.add_add

Modification history

2026-03-17 19:12

Mathlib/Analysis/Asymptotics/Defs.lean

feat(Mathlib/Analysis/Asymptotics/Defs): congr lemmas for IsBigO* (#35745) …

Added Asymptotics.IsBigO.add_add View on Github →