Commit 2026-08-17 10:30 90595330

View on Github →

refactor(Analysis/Asymptotics): use Monotone predicate in LinearGrowth lemmas (#42700) This is part of an effort to make lemmas that prove monotonicity more standard, explicit and discoverable, by using the Monotone predicate. Keeping this PR small for ease of code review.

Estimated changes