IndisputableMonolith.NumberTheory.Primes.Factorization

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.Primes.Basic
   3
   4/-!
   5# Factorization and valuations
   6
   7This file introduces a small, stable interface over Mathlib’s `Nat.factorization`.
   8
   9Primary goal: define a repo-local `vp` (“exponent of `p` in `n`”) and provide a few reusable
  10algebraic laws (`vp_mul`, `vp_pow`) that downstream prime work (squarefree, Möbius, etc.) can build on.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace NumberTheory
  15namespace Primes
  16
  17open Nat
  18
  19/-- `vp p n` is the exponent of `p` in the prime factorization of `n`
  20(implemented as `n.factorization p`). -/
  21def vp (p n : ℕ) : ℕ := n.factorization p
  22
  23@[simp] theorem vp_def (p n : ℕ) : vp p n = n.factorization p := rfl
  24
  25/-! ### `Nat.factorization` wrappers -/
  26
  27/-- Wrapper: factorization of a product (for nonzero factors). -/
  28theorem factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
  29    (a * b).factorization = a.factorization + b.factorization := by
  30  exact Nat.factorization_mul ha hb
  31
  32/-- Wrapper: factorization of a power. -/
  33theorem factorization_pow (n k : ℕ) : (n ^ k).factorization = k • n.factorization := by
  34  exact Nat.factorization_pow n k
  35
  36/-- For `a,b ≠ 0`, the `vp` exponent is additive under multiplication. -/
  37theorem vp_mul (p a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :
  38    vp p (a * b) = vp p a + vp p b := by
  39  simp [vp, Nat.factorization_mul ha hb]
  40
  41/-- The `vp` exponent scales under powers: `vp p (n^k) = k * vp p n`. -/
  42theorem vp_pow (p n k : ℕ) : vp p (n ^ k) = k * vp p n := by
  43  -- `factorization_pow` is unconditional (it handles `n = 0` internally).
  44  -- Evaluate at `p` and simplify `nsmul` on ℕ to multiplication.
  45  simp [vp, Nat.factorization_pow]
  46
  47/-! ### Boundary cases for `vp` -/
  48
  49/-- The exponent of any prime in 0 is 0 (by convention). -/
  50@[simp] theorem vp_zero (p : ℕ) : vp p 0 = 0 := by
  51  simp [vp]
  52
  53/-- The exponent of any prime in 1 is 0. -/
  54@[simp] theorem vp_one (p : ℕ) : vp p 1 = 0 := by
  55  simp [vp]
  56
  57/-- For a prime `p`, `vp p p = 1`. -/
  58theorem vp_prime_self {p : ℕ} (hp : Prime p) : vp p p = 1 := by
  59  have hp' : Nat.Prime p := (prime_iff p).1 hp
  60  simp [vp, hp'.factorization_self]
  61
  62/-- For distinct primes `p ≠ q`, `vp p q = 0`. -/
  63theorem vp_prime_ne {p q : ℕ} (_hp : Prime p) (hq : Prime q) (hne : p ≠ q) : vp p q = 0 := by
  64  have hq' : Nat.Prime q := (prime_iff q).1 hq
  65  simp only [vp]
  66  rw [hq'.factorization]
  67  simp [hne.symm]
  68
  69/-- For a prime `p` and `k ≥ 1`, `vp p (p^k) = k`. -/
  70theorem vp_prime_pow {p k : ℕ} (hp : Prime p) (_hk : 0 < k) : vp p (p ^ k) = k := by
  71  have hp' : Nat.Prime p := (prime_iff p).1 hp
  72  simp only [vp, Nat.factorization_pow, Finsupp.smul_apply, smul_eq_mul]
  73  rw [hp'.factorization_self]
  74  ring
  75
  76/-- For distinct primes `p ≠ q`, `vp p (q^k) = 0`. -/
  77theorem vp_prime_pow_ne {p q k : ℕ} (_hp : Prime p) (hq : Prime q) (hne : p ≠ q) :
  78    vp p (q ^ k) = 0 := by
  79  have hq' : Nat.Prime q := (prime_iff q).1 hq
  80  simp only [vp, Nat.factorization_pow, Finsupp.smul_apply, smul_eq_mul]
  81  rw [hq'.factorization]
  82  simp [hne.symm]
  83
  84/-! ### `vp` for GCD/LCM -/
  85
  86/-- The exponent of `p` in `gcd(a,b)` equals the minimum of the exponents.
  87For nonzero `a, b` and prime `p`. -/
  88theorem vp_gcd {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (p : ℕ) :
  89    vp p (Nat.gcd a b) = min (vp p a) (vp p b) := by
  90  simp only [vp]
  91  rw [Nat.factorization_gcd ha hb]
  92  rfl
  93
  94/-- The exponent of `p` in `lcm(a,b)` equals the maximum of the exponents.
  95For nonzero `a, b` and prime `p`. -/
  96theorem vp_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (p : ℕ) :
  97    vp p (Nat.lcm a b) = max (vp p a) (vp p b) := by
  98  simp only [vp]
  99  rw [Nat.factorization_lcm ha hb]
 100  rfl
 101
 102/-! ### Prime power characterization -/
 103
 104/-- If `n = p^k` for prime `p` and `k ≥ 1`, then `vp p n = k`. -/
 105theorem vp_eq_of_eq_prime_pow {n p k : ℕ} (hp : Prime p) (hk : 0 < k) (hn : n = p ^ k) :
 106    vp p n = k := by
 107  rw [hn]
 108  exact vp_prime_pow hp hk
 109
 110/-- If `n = p^k` for prime `p`, then `vp q n = 0` for any prime `q ≠ p`. -/
 111theorem vp_eq_zero_of_eq_prime_pow_ne {n p q k : ℕ} (hp : Prime p) (hq : Prime q)
 112    (hne : p ≠ q) (hn : n = p ^ k) : vp q n = 0 := by
 113  rw [hn]
 114  cases k with
 115  | zero => simp
 116  | succ k => exact vp_prime_pow_ne hq hp hne.symm
 117
 118/-! ### Divisibility and vp -/
 119
 120/-- `p^k ∣ n` iff `k ≤ vp p n` (for prime `p` and `n ≠ 0`). -/
 121theorem pow_dvd_iff_le_vp {p k n : ℕ} (hp : Prime p) (hn : n ≠ 0) :
 122    p ^ k ∣ n ↔ k ≤ vp p n := by
 123  have hp' : Nat.Prime p := (prime_iff p).1 hp
 124  simp only [vp]
 125  exact hp'.pow_dvd_iff_le_factorization hn
 126
 127/-- If `p ∤ n`, then `vp p n = 0`. -/
 128theorem vp_eq_zero_of_not_dvd {p n : ℕ} (h : ¬ p ∣ n) : vp p n = 0 := by
 129  simp only [vp]
 130  exact Nat.factorization_eq_zero_of_not_dvd h
 131
 132/-- For prime `p`, `p ∣ n` iff `vp p n ≥ 1` (for `n ≠ 0`). -/
 133theorem prime_dvd_iff_vp_pos {p n : ℕ} (hp : Prime p) (hn : n ≠ 0) :
 134    p ∣ n ↔ 0 < vp p n := by
 135  have hp' : Nat.Prime p := (prime_iff p).1 hp
 136  constructor
 137  · intro hdvd
 138    simp only [vp]
 139    exact hp'.factorization_pos_of_dvd hn hdvd
 140  · intro hvp
 141    rw [← pow_one p, pow_dvd_iff_le_vp hp hn]
 142    exact hvp
 143
 144end Primes
 145end NumberTheory
 146end IndisputableMonolith
 147