ArithmeticFunction.zeta_mul_zeta

@[blueprint  "zeta_mul_zeta"  (title := "zeta mul zeta")  (statement := /-- The Dirichlet convolution of $\zeta$ with itself is $\tau$ (the divisor count function). -/)  (proof := /--  By definition of $\zeta$, we have $\zeta(n) = 1$ for all $n \geq 1$. Thus, the Dirichlet convolution  $(\zeta * \zeta)(n)$ counts the number of ways to write $n$ as a product of two positive integers,  which is exactly the number of divisors of $n$, i.e., $\tau(n)$.  -/)]theorem zeta_mul_zeta : (ζ : ArithmeticFunction ℕ) * ζ = τ := by  ext n; unfold zeta tau sigma  simp only [mul_apply, coe_mk, mul_ite, mul_zero, mul_one, pow_zero, sum_const, smul_eq_mul]  have key : ∀ x ∈ n.divisorsAntidiagonal, (if x.2 = 0 then 0 else if x.1 = 0 then 0 else 1) = 1 := by    intro ⟨a, b⟩ hx    have := Nat.mem_divisorsAntidiagonal.mp hx    simp [mul_ne_zero_iff.mp (this.1 ▸ this.2)]  simp_rw [Finset.sum_congr rfl key, Finset.card_eq_sum_ones, Finset.sum_const]  simp only [smul_eq_mul, mul_one, ← Nat.map_div_right_divisors]  exact card_map { toFun := fun d ↦ (d, n / d), inj' := fun x x_1 ↦ congr_arg Prod.fst }