vp_mul

formal source

  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]