vp_pow

formal source

  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]