phiRung

formal source

  66
  67    For `n ≥ 1`, this is `Σ_p v_p(n) · phiRungPrime(p)`, where `v_p`
  68    is the `p`-adic valuation. -/
  69def phiRung (n : ℕ) : ℤ :=
  70  (Nat.factorization n).sum (fun p k => k * phiRungPrime p)
  71
  72/-- `phiRung(1) = 0` (the empty product). -/
  73@[simp] theorem phiRung_one : phiRung 1 = 0 := by
  74  unfold phiRung
  75  simp [Nat.factorization_one]
  76
  77/-- `phiRung(0) = 0` by convention (factorization of 0 is the zero
  78    finsupp). -/
  79@[simp] theorem phiRung_zero : phiRung 0 = 0 := by
  80  unfold phiRung
  81  simp [Nat.factorization_zero]
  82
  83/-- The phi-rung at a prime: `phiRung p = phiRungPrime p`. -/
  84theorem phiRung_prime {p : ℕ} (hp : Nat.Prime p) :
  85    phiRung p = phiRungPrime p := by
  86  unfold phiRung
  87  rw [Nat.Prime.factorization hp]
  88  simp
  89
  90/-- Multiplicativity (completely additive form): for positive `m, n`,
  91    `phiRung (m · n) = phiRung m + phiRung n`. -/
  92theorem phiRung_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
  93    phiRung (m * n) = phiRung m + phiRung n := by
  94  unfold phiRung
  95  rw [Nat.factorization_mul hm hn, Finsupp.sum_add_index']
  96  · intros
  97    push_cast
  98    ring
  99  · intros _ _ _