vp_gcd

formal source

  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 -/