Commit 2024-01-30 09:46 76b26e84

feat(Data/Nat/Prime): some lemmas on primes and powers (#10025) 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:

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.)