Prime numbers in the naturals and the integers

TODO: This file can probably be merged with Data/Nat/Int/NatPrime.lean.

theorem Nat.prime_iff_prime_int {p : ℕ} : Nat.Prime p ↔ Prime ↑p

theorem Nat.Prime.pow_inj {p : ℕ} {q : ℕ} {m : ℕ} {n : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (h : p ^ (m + 1) = q ^ (n + 1)) : p = q ∧ m = n

Two prime powers with positive exponents are equal only when the primes and the exponents are equal.

@[simp]

theorem Int.prime_ofNat_iff {n : ℕ} : Prime (OfNat.ofNat n) ↔ Nat.Prime (OfNat.ofNat n)

theorem Int.prime_two : Prime 2

theorem Int.prime_three : Prime 3