[Merged by Bors] - feat: implement rpow norm_num extension #9893
Conversation
|
This PR depends on #9875. The first four commits are borrowed from that PR, and I intend to rebase it once that PR lands. |
dwrensha
added
awaiting-review
dwrensha
removed
the
awaiting-review
|
(removed the "awaiting review" label while I fix the breakage in Bertrand.lean...) |
Mathlib/Tactic/NormNum/Pow.lean
Outdated
| /-- The `norm_num` extension which identifies expressions of the form `a ^ b`, | ||
| such that `norm_num` successfully recognises both `a` and `b`, with `b : ℤ`. -/ | ||
| @[norm_num (_ : α) ^ (_ : ℤ)] |
There was a problem hiding this comment.
Note that we also have #9875 that implements this. Nevermind, I see that was you!
There was a problem hiding this comment.
Yep. Please let me know if there's a better way to do stacked diffs.
There was a problem hiding this comment.
I know on gitlab I used to be able to have a PR pointing on the branch of another dependency PR, so that once the dependency is merged the PR would then point to master instead, and in the meantime you get a clean diff. I don't know if bors messes with that, though.
Edit: you can manually do that, it seems :)
There was a problem hiding this comment.
I don't think that's necessary, and it's a mess with our squash merges anyway. Putting things in the PR description is sufficient (I made an edit to that effect)
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
| guard <|← withNewMCtxDepth <| isDefEq f q(HPow.hPow (α := ℝ) (β := ℝ)) | ||
| haveI' : u =QL 0 := ⟨⟩ | ||
| haveI' : $α =Q ℝ := ⟨⟩ | ||
| haveI' h : $e =Q $a ^ $b := ⟨⟩ |
There was a problem hiding this comment.
I don't really care either way, but I'm curious what the advantage of haveI vs have is here.
There was a problem hiding this comment.
Me too! I'm just copying what I see in other extensions.
Mathlib/NumberTheory/Bertrand.lean
Outdated
| · positivity | ||
| · positivity | ||
| · positivity |
There was a problem hiding this comment.
Where did these side-goals come from?
There was a problem hiding this comment.
They come from the removal of <;> norm_num1 above. Two of them could be norm_num1.
I've moved them inline now, to make the proof structure more clear.
There was a problem hiding this comment.
done in 33546e9
(oops, I meant for this comment to apply to the other thread #9893 (comment) )
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on:
|
dwrensha
added
the
awaiting-review
| let e' : Q(ℝ) := q(($a ^ (-($nb : ℤ)))) | ||
| match ← derive e' with |
There was a problem hiding this comment.
This one can probably be inlined too
|
✌️ dwrensha can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors r+ |
* Implements a norm_num extension for `a ^ b` where `a` and `b` are reals. Unlike in the mathlib3 version, there is no restriction on the positivity of `a`. * Moves commented-out tests from test/norm_num_ext.lean into a new file test/norm_num_rpow.lean, to keep the dependencies of norm_num_ext.lean lightweight. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Build failed (retrying...): |
* Implements a norm_num extension for `a ^ b` where `a` and `b` are reals. Unlike in the mathlib3 version, there is no restriction on the positivity of `a`. * Moves commented-out tests from test/norm_num_ext.lean into a new file test/norm_num_rpow.lean, to keep the dependencies of norm_num_ext.lean lightweight. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
a ^ bwhereaandbare reals. Unlike in the mathlib3 version, there is no restriction on the positivity ofa.