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] - feat: More rpow
lemmas
#9108
Conversation
A bunch of easy lemmas about `Real.pow` and the golf of existing lemmas with them. Also rename `log_le_log` to `log_le_log_iff` and `log_le_log'` to `log_le_log`. Those misnames caused several proofs to bother with side conditions they didn't need. From LeanAPAP
#align real.rpow_int_cast Real.rpow_int_cast | ||
|
||
@[simp, norm_cast] | ||
theorem rpow_nat_cast (x : ℝ) (n : ℕ) : x ^ (n : ℝ) = x ^ n := by simpa using rpow_int_cast x n |
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.
Whats with these being nat_cast
vs natCast
elsewhere?
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.
We've hardly decided on a convention. I'm personally in favor of natCast
(and the poll a few months back agrees with me) but most lemmas have been ported as nat_cast
. This lemma is just moving, so I'm not changing its name. However I'm naming the new ones using natCast
.
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.
bors d+
Thanks!
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
bors merge |
A bunch of easy lemmas about `Real.pow` and the golf of existing lemmas with them. Also rename `log_le_log` to `log_le_log_iff` and `log_le_log'` to `log_le_log`. Those misnames caused several proofs to bother with side conditions they didn't need. From LeanAPAP
Build failed (retrying...):
|
A bunch of easy lemmas about `Real.pow` and the golf of existing lemmas with them. Also rename `log_le_log` to `log_le_log_iff` and `log_le_log'` to `log_le_log`. Those misnames caused several proofs to bother with side conditions they didn't need. From LeanAPAP
Pull request successfully merged into master. Build succeeded: |
rpow
lemmasrpow
lemmas
A bunch of easy lemmas about
Real.pow
and the golf of existing lemmas with them.Also rename
log_le_log
tolog_le_log_iff
andlog_le_log'
tolog_le_log
. Those misnames caused several proofs to bother with side conditions they didn't need.From LeanAPAP