factorization_mul

formal source

  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