Commit 2023-12-25 16:17 0a89f462

View on Github →

chore: Deprecate pow monotonicity lemmas (#9235) Add deprecated aliases for all the lemmas removed in #9095 and fix a few renames that were botched.

Estimated changes

added theorem Monotone.pow_const
deleted theorem Monotone.pow_right
added theorem pow_left_mono
deleted theorem pow_mono_right