chore(Data/Nat/Prime): split Defs; rearrange Basic (#18233)

This PR reduces the theory included with `Data/Nat/Prime/Defs.lean`, in particular allowing us to define `CharP` without needing theory on ordered monoids. Most of the contents got moved to `Basic.lean`, which would increase the downstream imports for quite a few file. So in turn I split up `Basic.lean` based on the imports and logical structure:
 * Results related to the factorial go to `Prime/Factorial.lean`
 * Results related to integers go to `Prime/Int.lean` (which should probably be merged with `Data/Int/NatPrime.lean)
 * The proof that there are infinitely many primes goes to `Prime/Infinite.lean`
 * Some results on powers of prime that needed a higher amount of ordered monoid theory go to `Prime/Pow.lean`

This is not a universal import win, since some files that imported `Defs.lean` now need to import `Basic.lean` instead, but I think that's worth it for keeping `Defs` files succinct.

Author: Vierkantor

Archive/Imo/Imo2019Q4.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import Mathlib.Data.Nat.Factorial.BigOperators
 import Mathlib.Data.Nat.Multiplicity
-import Mathlib.Data.Nat.Prime.Basic
+import Mathlib.Data.Nat.Prime.Int
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.GCongr
 

Mathlib.lean

@@ -2544,6 +2544,10 @@ import Mathlib.Data.Nat.PartENat
 import Mathlib.Data.Nat.Periodic
 import Mathlib.Data.Nat.Prime.Basic
 import Mathlib.Data.Nat.Prime.Defs
+import Mathlib.Data.Nat.Prime.Factorial
+import Mathlib.Data.Nat.Prime.Infinite
+import Mathlib.Data.Nat.Prime.Int
+import Mathlib.Data.Nat.Prime.Pow
 import Mathlib.Data.Nat.PrimeFin
 import Mathlib.Data.Nat.Set
 import Mathlib.Data.Nat.Size

Mathlib/Algebra/Order/Floor/Prime.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yuyang Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuyang Zhao
 -/
-import Mathlib.Data.Nat.Prime.Basic
+import Mathlib.Data.Nat.Prime.Infinite
 import Mathlib.Topology.Algebra.Order.Floor
 
 /-!

Mathlib/Data/Int/NatPrime.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Bryan Gin-ge Chen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Lacker, Bryan Gin-ge Chen
 -/
+import Mathlib.Algebra.Group.Int
 import Mathlib.Data.Nat.Prime.Basic
 
 /-!

Mathlib/Data/Nat/Choose/Dvd.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Patrick Stevens
 -/
 import Mathlib.Data.Nat.Choose.Basic
-import Mathlib.Data.Nat.Prime.Basic
+import Mathlib.Data.Nat.Prime.Factorial
 
 /-!
 # Divisibility properties of binomial coefficients

Mathlib/Data/Nat/Factorization/PrimePow.lean

@@ -5,6 +5,7 @@ Authors: Bhavik Mehta
 -/
 import Mathlib.Algebra.IsPrimePow
 import Mathlib.Data.Nat.Factorization.Basic
+import Mathlib.Data.Nat.Prime.Pow
 
 /-!
 # Prime powers and factorizations

Mathlib/Data/Nat/Factors.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Algebra.BigOperators.Ring.List
 import Mathlib.Data.Nat.GCD.Basic
-import Mathlib.Data.Nat.Prime.Defs
+import Mathlib.Data.Nat.Prime.Basic
 import Mathlib.Data.List.Prime
 import Mathlib.Data.List.Sort
 import Mathlib.Data.List.Perm.Subperm

Mathlib/Data/Nat/Prime/Basic.lean

@@ -4,29 +4,47 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Algebra.Associated.Basic
-import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
-import Mathlib.Algebra.Ring.Int
-import Mathlib.Data.Nat.Factorial.Basic
+import Mathlib.Algebra.Ring.Parity
 import Mathlib.Data.Nat.Prime.Defs
-import Mathlib.Order.Bounds.Basic
 
 /-!
-## Notable Theorems
+# Prime numbers
 
-- `Nat.exists_infinite_primes`: Euclid's theorem that there exist infinitely many prime numbers.
-  This also appears as `Nat.not_bddAbove_setOf_prime` and `Nat.infinite_setOf_prime` (the latter
-  in `Data.Nat.PrimeFin`).
+This file develops the theory of prime numbers: natural numbers `p ≥ 2` whose only divisors are
+`p` and `1`.
 
 -/
 
-
 open Bool Subtype
 
 open Nat
 
 namespace Nat
 variable {n : ℕ}
 
+theorem prime_mul_iff {a b : ℕ} : Nat.Prime (a * b) ↔ a.Prime ∧ b = 1 ∨ b.Prime ∧ a = 1 := by
+  simp only [irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]
+
+theorem not_prime_mul {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Prime (a * b) := by
+  simp [prime_mul_iff, _root_.not_or, *]
+
+theorem not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n :=
+  h ▸ not_prime_mul h₁ h₂
+
+theorem Prime.dvd_iff_eq {p a : ℕ} (hp : p.Prime) (a1 : a ≠ 1) : a ∣ p ↔ p = a := by
+  refine ⟨?_, by rintro rfl; rfl⟩
+  rintro ⟨j, rfl⟩
+  rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
+  · exact mul_one _
+  · exact (a1 rfl).elim
+
+theorem Prime.eq_two_or_odd {p : ℕ} (hp : Prime p) : p = 2 ∨ p % 2 = 1 :=
+  p.mod_two_eq_zero_or_one.imp_left fun h =>
+    ((hp.eq_one_or_self_of_dvd 2 (dvd_of_mod_eq_zero h)).resolve_left (by decide)).symm
+
+theorem Prime.eq_two_or_odd' {p : ℕ} (hp : Prime p) : p = 2 ∨ Odd p :=
+  Or.imp_right (fun h => ⟨p / 2, (div_add_mod p 2).symm.trans (congr_arg _ h)⟩) hp.eq_two_or_odd
+
 section
 
 theorem Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2)
@@ -78,26 +96,6 @@ theorem dvd_of_forall_prime_mul_dvd {a b : ℕ}
   obtain ⟨p, hp⟩ := exists_prime_and_dvd ha
   exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)
 
-/-- Euclid's theorem on the **infinitude of primes**.
-Here given in the form: for every `n`, there exists a prime number `p ≥ n`. -/
-theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Prime p :=
-  let p := minFac (n ! + 1)
-  have f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _
-  have pp : Prime p := minFac_prime f1
-  have np : n ≤ p :=
-    le_of_not_ge fun h =>
-      have h₁ : p ∣ n ! := dvd_factorial (minFac_pos _) h
-      have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
-      pp.not_dvd_one h₂
-  ⟨p, np, pp⟩
-
-/-- A version of `Nat.exists_infinite_primes` using the `BddAbove` predicate. -/
-theorem not_bddAbove_setOf_prime : ¬BddAbove { p | Prime p } := by
-  rw [not_bddAbove_iff]
-  intro n
-  obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ
-  exact ⟨p, hp, hi⟩
-
 theorem Prime.even_iff {p : ℕ} (hp : Prime p) : Even p ↔ p = 2 := by
   rw [even_iff_two_dvd, prime_dvd_prime_iff_eq prime_two hp, eq_comm]
 
@@ -159,18 +157,6 @@ theorem Prime.pow_eq_iff {p a k : ℕ} (hp : p.Prime) : a ^ k = p ↔ a = p ∧
   rw [← h] at hp
   rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]
 
-theorem pow_minFac {n k : ℕ} (hk : k ≠ 0) : (n ^ k).minFac = n.minFac := by
-  rcases eq_or_ne n 1 with (rfl | hn)
-  · simp
-  have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff hk).1 hk')
-  apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
-  apply
-    minFac_le_of_dvd (minFac_prime hnk).two_le
-      ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))
-
-theorem Prime.pow_minFac {p k : ℕ} (hp : p.Prime) (hk : k ≠ 0) : (p ^ k).minFac = p := by
-  rw [Nat.pow_minFac hk, hp.minFac_eq]
-
 theorem Prime.mul_eq_prime_sq_iff {x y p : ℕ} (hp : p.Prime) (hx : x ≠ 1) (hy : y ≠ 1) :
     x * y = p ^ 2 ↔ x = p ∧ y = p := by
   refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => h₁.symm ▸ h₂.symm ▸ (sq _).symm⟩
@@ -197,14 +183,6 @@ theorem Prime.mul_eq_prime_sq_iff {x y p : ℕ} (hp : p.Prime) (hx : x ≠ 1) (h
     rw [sq, Nat.mul_right_eq_self_iff (Nat.mul_pos hp.pos hp.pos : 0 < a * a)] at h
     exact h
 
-theorem Prime.dvd_factorial : ∀ {n p : ℕ} (_ : Prime p), p ∣ n ! ↔ p ≤ n
-  | 0, _, hp => iff_of_false hp.not_dvd_one (not_le_of_lt hp.pos)
-  | n + 1, p, hp => by
-    rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
-    exact
-      ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
-        (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩
-
 theorem Prime.coprime_pow_of_not_dvd {p m a : ℕ} (pp : Prime p) (h : ¬p ∣ a) : Coprime a (p ^ m) :=
   (pp.coprime_iff_not_dvd.2 h).symm.pow_right _
 
@@ -269,33 +247,4 @@ theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : Prime p) {
   exact hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h)
     fun h : p ∣ n / p ^ l => Or.inr <| mul_dvd_of_dvd_div hpn h
 
-theorem prime_iff_prime_int {p : ℕ} : p.Prime ↔ _root_.Prime (p : ℤ) :=
-  ⟨fun hp =>
-    ⟨Int.natCast_ne_zero_iff_pos.2 hp.pos, mt Int.isUnit_iff_natAbs_eq.1 hp.ne_one, fun a b h => by
-      rw [← Int.dvd_natAbs, Int.natCast_dvd_natCast, Int.natAbs_mul, hp.dvd_mul] at h
-      rwa [← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]⟩,
-    fun hp =>
-    Nat.prime_iff.2
-      ⟨Int.natCast_ne_zero.1 hp.1,
-        (mt Nat.isUnit_iff.1) fun h => by simp [h, not_prime_one] at hp, fun a b => by
-        simpa only [Int.natCast_dvd_natCast, (Int.ofNat_mul _ _).symm] using hp.2.2 a b⟩⟩
-
-/-- Two prime powers with positive exponents are equal only when the primes and the
-exponents are equal. -/
-lemma Prime.pow_inj {p q m n : ℕ} (hp : p.Prime) (hq : q.Prime)
-    (h : p ^ (m + 1) = q ^ (n + 1)) : p = q ∧ m = n := by
-  have H := dvd_antisymm (Prime.dvd_of_dvd_pow hp <| h ▸ dvd_pow_self p (succ_ne_zero m))
-    (Prime.dvd_of_dvd_pow hq <| h.symm ▸ dvd_pow_self q (succ_ne_zero n))
-  exact ⟨H, succ_inj'.mp <| Nat.pow_right_injective hq.two_le (H ▸ h)⟩
-
 end Nat
-
-namespace Int
-
-theorem prime_two : Prime (2 : ℤ) :=
-  Nat.prime_iff_prime_int.mp Nat.prime_two
-
-theorem prime_three : Prime (3 : ℤ) :=
-  Nat.prime_iff_prime_int.mp Nat.prime_three
-
-end Int

Mathlib/Data/Nat/Prime/Defs.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Batteries.Data.Nat.Gcd
-import Mathlib.Algebra.Prime.Lemmas
-import Mathlib.Algebra.Ring.Parity
+import Mathlib.Algebra.Prime.Defs
+import Mathlib.Algebra.Ring.Nat
+import Mathlib.Order.Lattice
 
 /-!
 # Prime numbers
@@ -161,29 +162,6 @@ theorem prime_dvd_prime_iff_eq {p q : ℕ} (pp : p.Prime) (qp : q.Prime) : p ∣
 theorem Prime.not_dvd_one {p : ℕ} (pp : Prime p) : ¬p ∣ 1 :=
   Irreducible.not_dvd_one pp
 
-theorem prime_mul_iff {a b : ℕ} : Nat.Prime (a * b) ↔ a.Prime ∧ b = 1 ∨ b.Prime ∧ a = 1 := by
-  simp only [irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]
-
-theorem not_prime_mul {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Prime (a * b) := by
-  simp [prime_mul_iff, _root_.not_or, *]
-
-theorem not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n :=
-  h ▸ not_prime_mul h₁ h₂
-
-theorem Prime.dvd_iff_eq {p a : ℕ} (hp : p.Prime) (a1 : a ≠ 1) : a ∣ p ↔ p = a := by
-  refine ⟨?_, by rintro rfl; rfl⟩
-  rintro ⟨j, rfl⟩
-  rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
-  · exact mul_one _
-  · exact (a1 rfl).elim
-
-theorem Prime.eq_two_or_odd {p : ℕ} (hp : Prime p) : p = 2 ∨ p % 2 = 1 :=
-  p.mod_two_eq_zero_or_one.imp_left fun h =>
-    ((hp.eq_one_or_self_of_dvd 2 (dvd_of_mod_eq_zero h)).resolve_left (by decide)).symm
-
-theorem Prime.eq_two_or_odd' {p : ℕ} (hp : Prime p) : p = 2 ∨ Odd p :=
-  Or.imp_right (fun h => ⟨p / 2, (div_add_mod p 2).symm.trans (congr_arg _ h)⟩) hp.eq_two_or_odd
-
 section MinFac
 
 theorem minFac_lemma (n k : ℕ) (h : ¬n < k * k) : sqrt n - k < sqrt n + 2 - k :=

Mathlib/Data/Nat/Prime/Factorial.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
+import Mathlib.Data.Nat.Factorial.Basic
+import Mathlib.Data.Nat.Prime.Defs
+
+/-!
+# Prime natural numbers and the factorial operator
+
+-/
+
+open Bool Subtype
+
+open Nat
+
+namespace Nat
+
+theorem Prime.dvd_factorial : ∀ {n p : ℕ} (_ : Prime p), p ∣ n ! ↔ p ≤ n
+  | 0, _, hp => iff_of_false hp.not_dvd_one (not_le_of_lt hp.pos)
+  | n + 1, p, hp => by
+    rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
+    exact
+      ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
+        (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩
+
+end Nat