vp_one

formal source

  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]
  73  rw [hp'.factorization_self]
  74  ring
  75
  76/-- For distinct primes `p ≠ q`, `vp p (q^k) = 0`. -/
  77theorem vp_prime_pow_ne {p q k : ℕ} (_hp : Prime p) (hq : Prime q) (hne : p ≠ q) :
  78    vp p (q ^ k) = 0 := by
  79  have hq' : Nat.Prime q := (prime_iff q).1 hq
  80  simp only [vp, Nat.factorization_pow, Finsupp.smul_apply, smul_eq_mul]
  81  rw [hq'.factorization]
  82  simp [hne.symm]
  83
  84/-! ### `vp` for GCD/LCM -/