IndisputableMonolith.NumberTheory.Primes.Squarefree

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.Primes.Factorization
   3
   4/-!
   5# Squarefree (via `vp`)
   6
   7This file connects the standard `Squarefree` predicate on naturals to the repo-local valuation
   8`vp p n` (exponent of `p` in `n.factorization`).
   9-/
  10
  11namespace IndisputableMonolith
  12namespace NumberTheory
  13namespace Primes
  14
  15open Nat
  16
  17/-- A nonzero natural `n` is squarefree iff every prime exponent in its factorization is ≤ 1.
  18
  19This is a thin wrapper around Mathlib’s `Nat.squarefree_iff_factorization_le_one`. -/
  20theorem squarefree_iff_vp_le_one {n : ℕ} (hn : n ≠ 0) :
  21    Squarefree n ↔ ∀ p : ℕ, vp p n ≤ 1 := by
  22  simpa [vp] using (Nat.squarefree_iff_factorization_le_one (n := n) hn)
  23
  24/-- Prime-restricted version: for `n ≠ 0`, squarefree iff `vp p n ≤ 1` for all primes `p`. -/
  25theorem squarefree_iff_vp_le_one_of_prime {n : ℕ} (hn : n ≠ 0) :
  26    Squarefree n ↔ ∀ p : ℕ, Prime p → vp p n ≤ 1 := by
  27  constructor
  28  · intro hsq p hp
  29    -- Use the non-restricted statement.
  30    have hall : ∀ p : ℕ, vp p n ≤ 1 := (squarefree_iff_vp_le_one (n := n) hn).1 hsq
  31    exact hall p
  32  · intro hprime
  33    -- Prove the non-restricted bound, then use Mathlib's characterization.
  34    refine (squarefree_iff_vp_le_one (n := n) hn).2 (fun p => ?_)
  35    by_cases hp : Nat.Prime p
  36    · have hp' : Prime p := (prime_iff p).2 hp
  37      exact hprime p hp'
  38    · -- Non-prime `p` contributes `0` to the factorization.
  39      have hvp : vp p n = 0 := by
  40        simp [vp, Nat.factorization_eq_zero_of_not_prime n hp]
  41      -- Rewrite the goal and discharge it.
  42      rw [hvp]
  43      exact Nat.zero_le 1
  44
  45/-- **Dichotomy**: for squarefree `n`, every prime exponent is exactly 0 or 1. -/
  46theorem squarefree_vp_dichotomy {n : ℕ} (hn : n ≠ 0) (hsq : Squarefree n) (p : ℕ) :
  47    vp p n = 0 ∨ vp p n = 1 := by
  48  have hvp_le : vp p n ≤ 1 := (squarefree_iff_vp_le_one (n := n) hn).1 hsq p
  49  omega
  50
  51/-- For squarefree `n` and prime `p`, `p ∣ n` iff `vp p n = 1`. -/
  52theorem squarefree_prime_dvd_iff_vp_eq_one {n p : ℕ} (hn : n ≠ 0) (hsq : Squarefree n)
  53    (hp : Prime p) : p ∣ n ↔ vp p n = 1 := by
  54  have hp' : Nat.Prime p := (prime_iff p).1 hp
  55  constructor
  56  · intro hdvd
  57    have hpos : 0 < vp p n := by
  58      simp only [vp]
  59      exact hp'.factorization_pos_of_dvd hn hdvd
  60    have hle : vp p n ≤ 1 := (squarefree_iff_vp_le_one (n := n) hn).1 hsq p
  61    omega
  62  · intro hvp_eq
  63    -- Use the pow_dvd_iff characterization: p^k ∣ n iff k ≤ vp p n
  64    have hdvd : p ^ 1 ∣ n := by
  65      rw [hp'.pow_dvd_iff_le_factorization hn]
  66      simp only [vp] at hvp_eq
  67      omega
  68    simpa using hdvd
  69
  70/-- For squarefree `n` and prime `p`, `¬ p ∣ n` iff `vp p n = 0`. -/
  71theorem squarefree_prime_not_dvd_iff_vp_eq_zero {n p : ℕ} (hn : n ≠ 0) (hsq : Squarefree n)
  72    (hp : Prime p) : ¬ p ∣ n ↔ vp p n = 0 := by
  73  rw [squarefree_prime_dvd_iff_vp_eq_one hn hsq hp]
  74  have hdich := squarefree_vp_dichotomy hn hsq p
  75  constructor
  76  · intro hne1
  77    rcases hdich with h0 | h1
  78    · exact h0
  79    · exact False.elim (hne1 h1)
  80  · intro h0 h1
  81    omega
  82
  83/-! ### Squarefree products -/
  84
  85/-- The product of coprime squarefree numbers is squarefree. -/
  86theorem squarefree_mul_of_coprime {m n : ℕ} (hm : Squarefree m) (hn : Squarefree n)
  87    (hcop : Nat.Coprime m n) : Squarefree (m * n) := by
  88  exact (Nat.squarefree_mul hcop).mpr ⟨hm, hn⟩
  89
  90/-- A prime is squarefree. -/
  91theorem squarefree_prime {p : ℕ} (hp : Prime p) : Squarefree p := by
  92  have hp' : Nat.Prime p := (prime_iff p).1 hp
  93  exact hp'.squarefree
  94
  95/-- 1 is squarefree. -/
  96theorem squarefree_one' : Squarefree 1 := by
  97  exact _root_.squarefree_one
  98
  99end Primes
 100end NumberTheory
 101end IndisputableMonolith
 102