ArithmeticFunction.d_apply

@[blueprint  "d_apply"  (title := "d apply")  (statement := /-- (1.25) in Iwaniec-Kowalski: a formula for $d_k$ for all $n$. -/)  (proof := /--  The function $d_k$ is multiplicative, so to compute $d_k(n)$ for a general natural number $n$, we can factor $n$ into its prime power decomposition: $n = p_1^{a_1} p_2^{a_2} ... p_m^{a_m}$. Since $d_k$ is multiplicative, we have:   \[  d_k(n) = d_k(p_1^{a_1}) \cdot d_k(p_2^{a_2}) \cdot ... \cdot d_k(p_m^{a_m})  \]   Using the explicit formula for prime powers from the previous theorem, we can substitute to get:   \[  d_k(n) = \prod_{i=1}^{m} (a_i + k - 1).choose (k - 1)  \]   This gives us a complete formula for $d_k(n)$ in terms of the prime factorization of $n$.  -/)]lemma d_apply {k n : ℕ} (hk : 0 < k) (hn : n ≠ 0) :    d k n = ∏ p ∈ n.primeFactors, (n.factorization p + k - 1).choose (k - 1) := by  have hmult : (d k).IsMultiplicative := d_isMultiplicative k  rw [hmult.multiplicative_factorization (d k) hn, prod_factorization_eq_prod_primeFactors]  apply prod_congr rfl (fun p hp => ?_)  simpa using d_apply_prime_pow hk (prime_of_mem_primeFactors hp) _