Prime numbers

This file develops the theory of prime numbers: natural numbers p ≥ 2 whose only divisors are p and 1.

theorem Nat.pow_minFac {n : ℕ} {k : ℕ} (hk : k ≠ 0) : (n ^ k).minFac = n.minFac

theorem Nat.Prime.pow_minFac {p : ℕ} {k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) : (p ^ k).minFac = p