[Merged by Bors] - feat(Data/Nat/Prime): some lemmas on primes and powers #10025
Conversation
MichaelStollBayreuth
added
awaiting-review
MichaelStollBayreuth
changed the title
MichaelStollBayreuth
changed the title
MichaelStollBayreuth
changed the title
Mathlib/Data/Nat/Prime.lean
Outdated
| @@ -736,6 +738,14 @@ theorem prime_iff_prime_int {p : ℕ} : p.Prime ↔ _root_.Prime (p : ℤ) := | |||
| simpa only [Int.coe_nat_dvd, (Int.ofNat_mul _ _).symm] using hp.2.2 a b⟩⟩ | |||
| #align nat.prime_iff_prime_int Nat.prime_iff_prime_int | |||
|
|
|||
| /-- Two prime powers with positive exponents are equal only when the primes and the | |||
| exponents are equal. -/ | |||
| lemma Prime.pow_injective {p q m n : ℕ} (hp : p.Prime) (hq : q.Prime) | |||
There was a problem hiding this comment.
Theorems whose name ends with "injective" usually have Injective as their conclusion. Probably _inj is better. You might also want _inj_left (p=q) and _inj_right (m=n) (assuming I got my left and right correct)
There was a problem hiding this comment.
I'll change "injective" to "inj".
Loogling for "_inj_left" shows that it is not consistent, with a 7-5 majority concluding equality for the first argument. There are quite a few more with "_left_inj" (I didn't try to count here).
Nat.pow_right_injective gives the "_inv_right" version (using Nat.Prime.two_le); would the version for the second argument still be good to have (essentially replacing 2 ≤ n with n.Prime)?
Nat.pow_left_injective is more general (no restriction to primes), so the left version is maybe not necessary.
|
Thanks! bors merge |
github-actions
bot
added
ready-to-merge
This is the first PR in a sequence that adds auxiliary lemmas from the [EulerProducts](https://github.com/MichaelStollBayreuth/EulerProducts) project to Mathlib. It adds two lemmas on prime numbers and powers: ```lean lemma Nat.Prime.one_le {p : ℕ} (hp : p.Prime) : 1 ≤ p lemma Nat.Prime.pow_injective {p q m n : ℕ} (hp : p.Prime) (hq : q.Prime) (h : p ^ (m + 1) = q ^ (n + 1)) : p = q ∧ m = n ``` (The first one is for discoverability by `exact?` in cases one needs `1 ≤ p`.)
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
This is the first PR in a sequence that adds auxiliary lemmas from the EulerProducts project to Mathlib.
It adds two lemmas on prime numbers and powers:
(The first one is for discoverability by
exact?in cases one needs1 ≤ p.)