phiRung_zero

formal source

  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 _ _ _
 100    push_cast
 101    ring
 102
 103/-- The phi-rung at a prime power: `phiRung (p^k) = k · phiRungPrime p`. -/
 104theorem phiRung_prime_pow {p : ℕ} (hp : Nat.Prime p) (k : ℕ) :
 105    phiRung (p ^ k) = (k : ℤ) * phiRungPrime p := by
 106  induction k with
 107  | zero => simp
 108  | succ k ih =>
 109    have hpk : p ^ k ≠ 0 := pow_ne_zero _ hp.ne_zero