vp_prime_self

formal source

  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 -/
  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 : ℕ) :