vp_lcm

formal source

  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