ArithmeticFunction.d_apply_prime_pow

@[blueprint  "d_apply_prime_pow"  (title := "d apply prime pow")  (statement := /-- Explicit formula: $d_k (p^a) = (a + k - 1).choose (k - 1)$ for prime $p$ and $k \geq 1$. -/)  (proof := /--  The function $d_k$ counts the number of ways to write a natural number as an ordered product of $k$ natural numbers. For a prime power $p^a$, the number of ways to factor it into $k$ factors corresponds to the number of non-negative integer solutions to the equation $x_1 + x_2 + ... + x_k = a$, where each $x_i$ represents the exponent of $p$ in the factorization of the corresponding factor. This is a classic combinatorial problem, and the number of solutions is given by the formula $(a + k - 1).choose (k - 1)$, which counts the ways to distribute $a$ indistinguishable items (the prime factors) into $k$ distinguishable boxes (the factors).  -/)]theorem d_apply_prime_pow {k : ℕ} (hk : 0 < k) {p : ℕ} (hp : p.Prime) (a : ℕ) :    d k (p ^ a) = (a + k - 1).choose (k - 1) := by  obtain ⟨k', rfl⟩ := exists_eq_succ_of_ne_zero (Nat.ne_of_gt hk)  induction k' generalizing a with  | zero => simp [d_one, hp.ne_zero]  | succ k' ih =>      rw [d_succ, mul_zeta_apply, sum_divisors_prime_pow hp]      simp_rw [fun i ↦ ih i (succ_pos _)]      simpa [add_assoc, add_left_comm, add_comm] using sum_range_add_choose a k'