IndisputableMonolith.NumberTheory.Primes.Wrappers

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.Primes.Basic
   3
   4/-!
   5# Mathlib wrappers (prime toolkit)
   6
   7This file provides **stable, repo-local names** for a small set of high-value prime theorems that
   8already exist in Mathlib.
   9
  10Rationale: downstream code should depend on `IndisputableMonolith.NumberTheory.Primes.…` names so we
  11can refactor imports and interfaces without chasing Mathlib API changes.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace NumberTheory
  16namespace Primes
  17
  18/-! ### Infinitude of primes (Euclid) -/
  19
  20/-- For every `n`, there exists a prime `p ≥ n`. -/
  21theorem exists_prime_ge (n : ℕ) : ∃ p, n ≤ p ∧ Prime p := by
  22  simpa [Prime] using Nat.exists_infinite_primes n
  23
  24/-! ### Euclid's lemma -/
  25
  26/-- Euclid's lemma (iff form): if `p` is prime, then `p ∣ a*b ↔ p ∣ a ∨ p ∣ b`. -/
  27theorem prime_dvd_mul_iff {p a b : ℕ} (hp : Prime p) : p ∣ a * b ↔ p ∣ a ∨ p ∣ b := by
  28  simpa [Prime] using (Nat.Prime.dvd_mul (p := p) (m := a) (n := b) hp)
  29
  30/-- Euclid's lemma (implication form): if `p` is prime and `p ∣ a*b`, then `p ∣ a ∨ p ∣ b`. -/
  31theorem euclid_lemma {p a b : ℕ} (hp : Prime p) (h : p ∣ a * b) : p ∣ a ∨ p ∣ b :=
  32  (prime_dvd_mul_iff (p := p) (a := a) (b := b) hp).1 h
  33
  34/-! ### Prime divisibility and powers -/
  35
  36/-- If `p` is prime and `p ∣ a^n`, then `p ∣ a`. -/
  37theorem prime_dvd_of_dvd_pow {p a n : ℕ} (hp : Prime p) (h : p ∣ a ^ n) : p ∣ a :=
  38  ((prime_iff p).1 hp).dvd_of_dvd_pow h
  39
  40/-- If `p,q` are prime and `p ∣ q^m`, then `p = q`. -/
  41theorem prime_eq_of_dvd_pow {m p q : ℕ} (hp : Prime p) (hq : Prime q) (h : p ∣ q ^ m) : p = q := by
  42  have hp' : Nat.Prime p := (prime_iff p).1 hp
  43  have hq' : Nat.Prime q := (prime_iff q).1 hq
  44  exact Nat.prime_eq_prime_of_dvd_pow (m := m) hp' hq' h
  45
  46/-! ### Prime power divisors -/
  47
  48/-- Classification: divisors of a prime power are themselves prime powers. -/
  49theorem dvd_prime_pow_iff {p i m : ℕ} (hp : Prime p) : i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k := by
  50  simpa [Prime] using (Nat.dvd_prime_pow (p := p) (m := m) (i := i) hp)
  51
  52/-! ### Coprimality and primes -/
  53
  54/-- A prime `p` is coprime to `n` iff `p` does not divide `n`. -/
  55theorem coprime_iff_not_dvd_of_prime {p n : ℕ} (hp : Prime p) :
  56    Nat.Coprime p n ↔ ¬ p ∣ n := by
  57  have hp' : Nat.Prime p := (prime_iff p).1 hp
  58  exact hp'.coprime_iff_not_dvd
  59
  60/-- Symmetric form: `n` is coprime to prime `p` iff `p` does not divide `n`. -/
  61theorem coprime_comm_iff_not_dvd_of_prime {p n : ℕ} (hp : Prime p) :
  62    Nat.Coprime n p ↔ ¬ p ∣ n := by
  63  rw [Nat.coprime_comm]
  64  exact coprime_iff_not_dvd_of_prime hp
  65
  66/-- A prime `p` divides `n` iff `gcd(p, n) = p`. -/
  67theorem prime_dvd_iff_gcd_eq {p n : ℕ} (hp : Prime p) :
  68    p ∣ n ↔ Nat.gcd p n = p := by
  69  have hp' : Nat.Prime p := (prime_iff p).1 hp
  70  constructor
  71  · intro hdvd
  72    exact Nat.gcd_eq_left hdvd
  73  · intro hgcd
  74    rw [← hgcd]
  75    exact Nat.gcd_dvd_right p n
  76
  77end Primes
  78end NumberTheory
  79end IndisputableMonolith
  80