-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: Deprecate pow monotonicity lemmas #9235
Conversation
Add deprecated aliases for all the lemmas removed in #9095
theorem Monotone.pow_right {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n | ||
theorem Monotone.pow_const {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n | ||
| 0 => by simpa using monotone_const | ||
| n + 1 => by | ||
simp_rw [pow_succ] | ||
exact hf.mul' (Monotone.pow_right hf _) | ||
#align monotone.pow_right Monotone.pow_right | ||
exact hf.mul' (Monotone.pow_const hf _) | ||
#align monotone.pow_right Monotone.pow_const |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These don't look like deprecations to me; can you split them to their own PR?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Those lemma renames were announced in #9095. I just messed up when doing so.
LGTM but I don't know how to verify that all aliases are there. |
You could check the list from the description of #9095 one by one. I copy-pasted it to get the aliases. |
Let's get it merged |
Add deprecated aliases for all the lemmas removed in #9095 and fix a few renames that were botched.
Pull request successfully merged into master. Build succeeded: |
Add deprecated aliases for all the lemmas removed in #9095 and fix a few renames that were botched.
See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Renaming.20monotonicity.20of.20powers.20lemmas