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(NumberTheory/Padics/PadicVal): Add padicValNat_mul_pow_left/right
#11354
Conversation
…ght` Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n`
padicValNat_prod_pow_left/right
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.
LGTM (see my suggestion below)
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.
I do wonder how often we'll have both [Fact p.Prime]
and [Fact q.Prime]
available but in any case there is nothing controversial here.
Thanks!
bors d+
✌️ gaetanserre can now approve this pull request. To approve and merge a pull request, simply reply with |
padicValNat_prod_pow_left/right
padicValNat_mul_pow_left/right
Co-authored-by: Oliver Nash <github@olivernash.org>
Co-authored-by: Oliver Nash <github@olivernash.org>
bors r+ |
…ht` (#11354) Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n` Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>
Build failed (retrying...): |
…ht` (#11354) Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n` Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>
Build failed (retrying...):
|
…ht` (#11354) Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n` Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
padicValNat_mul_pow_left/right
padicValNat_mul_pow_left/right
…ht` (#11354) Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n` Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>
…ht` (#11354) Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n` Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>
…ht` (#11354) Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n` Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>
…ht` (#11354) Add two theorems solving goals of this form: for any primes `p` and `q` such that `p != q`, `padicValNat p (p^n * q^m) = n` Co-authored-by: Gaëtan Serré <56162277+gaetanserre@users.noreply.github.com>
Add two theorems solving goals of this form: for any primes
p
andq
such thatp != q
,padicValNat p (p^n * q^m) = n