Prime numbers in the naturals and the integers

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

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

theorem Nat.Prime.pow_inj {p q m n : ℕ} (hp : Prime p) (hq : 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.

theorem Nat.Prime.pow_inj' {p q m n : ℕ} (hp : Prime p) (hq : Prime q) (hm : m ≠ 0) (hn : n ≠ 0) (h : p ^ m = q ^ n) : p = q ∧ m = n

Version of Nat.Prime.pow_inj with an explicit nonzero assumption on the exponents.

@[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